vault backup: 2025-03-10 08:24:43

Concurrent Systems/notes/2 - Fast mutex by Lamport.md

@@ -0,0 +1,77 @@
+Initial idea:
+```
+Initialize Y at ⊥, X at any value (e.g., 0)
+
+lock(i) :=
+	x <- i
+	if Y != ⊥ then FAIL
+	else Y <- i
+	if X = i then return
+	else FAIL
+
+ unlock(i) :=
+	 Y <- ⊥
+	 return
+```
+
+Problems:
+- we don't want the FAIL
+- it is possible to have an execution where nobody accesses its CS, if repeated forever it entails a deadlock
+
+```
+Initialize Y at ⊥, X at any value (e.g., 0)
+
+
+lock(i) :=
+	* FLAG[i] <- up
+	X <- i
+	if Y ≠ ⊥ then
+		FLAG[i] <- down
+		wait Y = ⊥
+		goto *
+	else Y <- i
+	
+	if X = i then return
+	else FLAG[i] <- down
+	
+	∀j.wait FLAG[j] = down
+	
+	if Y = i then return
+	else wait Y = ⊥
+	
+	goto *
+
+unlock(i) :=
+	Y <- ⊥
+	FLAG[i] <- down
+	return
+```
+
+##### MUTEX proof
+How can pi enter its CS?
+![[Pasted image 20250304084537.png]]
+
+![[Pasted image 20250304084901.png]]
+(*must finished before nel senso che $p_i$ deve aspettare $p_j$*)
+##### Deadlock freedom
+Let $p_i$ invoke lock
+- If it eventually wins -> √
+- If it is blocked forever, where can it be blocked?
+	1. In the second wait Y =  ⊥
+		- in this case, it read a value in Y different from i
+		- there is a $p_h$ that wrote Y after $p_i$
+		- let us consider the last of such $p_h \to$ it will eventually win
+	2. In the ∀j.wait FLAG[j] = down
+		- this wait cannot block a process forever
+		- if $pj$ doesn't lock, it flag is down
+		- if $pj$ doesn't find Y at ⊥, it puts its flag down
+		- if pj doesn't find X at j, it puts its flag down, otherwise pj enters its CS and eventually unlocks (flag down)
+	- 3. In the first wait Y = ⊥
+		- since pj read a value different from ⊥, there is at least one pk that wrote Y before (but has not yet unlocked)
+		- if $p_k$ eventually enters its CS -> ok, otherwise it must be blocked forever as well. Where?
+			- In the second wait Y = ⊥: but then there exists a $p_h$ that eventually enters its CS -> good
+			- In the ∀j.wait FLAG[j]=down: this wait cannot block a process forever
+
+![[Pasted image 20250304090219.png]]
+
+esercizio: prova che NON soddisfa starvation freedom