vault backup: 2025-03-10 17:25:21
This commit is contained in:
parent
33d49a9cc3
commit
0f9edce76b
3 changed files with 6 additions and 3 deletions
5
.obsidian/workspace.json
vendored
5
.obsidian/workspace.json
vendored
|
@ -34,9 +34,9 @@
|
||||||
"type": "pdf",
|
"type": "pdf",
|
||||||
"state": {
|
"state": {
|
||||||
"file": "Concurrent Systems/slides/class 3.pdf",
|
"file": "Concurrent Systems/slides/class 3.pdf",
|
||||||
"page": 10,
|
"page": 13,
|
||||||
"left": -26,
|
"left": -26,
|
||||||
"top": 499,
|
"top": 31,
|
||||||
"zoom": 0.57541567695962
|
"zoom": 0.57541567695962
|
||||||
},
|
},
|
||||||
"icon": "lucide-file-text",
|
"icon": "lucide-file-text",
|
||||||
|
@ -218,6 +218,7 @@
|
||||||
},
|
},
|
||||||
"active": "6edd4157a160e462",
|
"active": "6edd4157a160e462",
|
||||||
"lastOpenFiles": [
|
"lastOpenFiles": [
|
||||||
|
"Pasted image 20250310172134.png",
|
||||||
"Concurrent Systems/slides/class 3.pdf",
|
"Concurrent Systems/slides/class 3.pdf",
|
||||||
"Concurrent Systems/notes/3.md",
|
"Concurrent Systems/notes/3.md",
|
||||||
"Pasted image 20250310103703.png",
|
"Pasted image 20250310103703.png",
|
||||||
|
|
|
@ -229,7 +229,9 @@ unlock(i) :=
|
||||||
**Theorem:** if $p_i$ is in the CS, then $p_j$ cannot simultaneously be in the CS.
|
**Theorem:** if $p_i$ is in the CS, then $p_j$ cannot simultaneously be in the CS.
|
||||||
*Proof:* by contradiction.
|
*Proof:* by contradiction.
|
||||||
|
|
||||||
...
|
Let's consider the execution of $p_i$ leading to its CS:
|
||||||
|
![[Pasted image 20250310172134.png]]
|
||||||
|
|
||||||
|
|
||||||
#### Bounded bypass proof
|
#### Bounded bypass proof
|
||||||
**Lemma 1:** exactly after n CSs there is a reset of DATE.
|
**Lemma 1:** exactly after n CSs there is a reset of DATE.
|
||||||
|
|
BIN
Pasted image 20250310172134.png
Normal file
BIN
Pasted image 20250310172134.png
Normal file
Binary file not shown.
After Width: | Height: | Size: 71 KiB |
Loading…
Reference in a new issue