vault backup: 2025-03-03 19:41:59

Concurrent Systems/notes/Lezione1.md

@@ -231,4 +231,12 @@ Induction (true for ℓ+1, to be proved for ℓ):
 - If some $p_{y}$ will eventually set $A\_Y[ℓ+1]$ to $y$, then $p_x$ will eventually exit from its wait and pass to level ℓ+1
 
 - Otherwise, let $G = \{p_{i}: F[i] \geq ℓ+1\}$ and $L=\{p_{i}:F[i]<ℓ+1\}$
-	- if $p \in L$, it will never enter its ℓ+1-th loop (as it would write A_Y[ℓ+1])
+	- if $p \in L$, it will never enter its ℓ+1-th loop (as it would write $A_Y[ℓ+1]$ and it will unblock $p_x$, but we are assuming that it is blocked)
+	- all $p \in G$ will eventually win (by induction) and move to L
+		- $\to$ eventually, $p_{x}$ will be the only one in its ℓ+1-th loop, with all the other processes at level <ℓ+1
+		- $\to$ $p_{x}$ will eventually pass to level ℓ+1 and win (by induction)
+
+
+##### Peterson algorithm cost
+- $n$ MRSW registers of $\lceil \log_{2} n\rceil$ bits (FLAG)
+- $n-1$ MRMW