vault backup: 2025-03-24 09:14:23

.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",

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
+- 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