diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index fe2f714..bec7fe3 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -51,9 +51,9 @@ "type": "pdf", "state": { "file": "Concurrent Systems/slides/class 7.pdf", - "page": 1, + "page": 5, "left": -23, - "top": 56, + "top": 593, "zoom": 0.680522565320665 }, "icon": "lucide-file-text", diff --git a/Concurrent Systems/notes/7- MUTEX-free concurrency.md b/Concurrent Systems/notes/7- MUTEX-free concurrency.md index ceeeac7..8749839 100644 --- a/Concurrent Systems/notes/7- MUTEX-free concurrency.md +++ b/Concurrent Systems/notes/7- MUTEX-free concurrency.md @@ -41,7 +41,7 @@ We have: dir(i) := LAST <- i if DOOR = 0 then - retunr R + return R else DOOR <- 0 if LAST = i then @@ -52,4 +52,15 @@ dir(i) := With 2 processes, we can have: - one goes left and one goes right - one goes left and the other stops -- one goes right and the other stops \ No newline at end of file +- one goes right and the other stops + +#### Soundness theorem +this implementation satisfies the three requirements for the splitter + +*Proof:* +1. Not all processes can obtain R + - the door must have been closed and who closed the door cannot obtain R +2. not all processes can obtain L + - let us consider the last process that writes into LAST (this is an atomic register, so this is meaningful) + - if the door is closed, it receives R and √ +3. let $p_i$ be the first process that receives S \ No newline at end of file