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

Concurrent Systems/notes/Lezione1.md

@@ -230,4 +230,5 @@ 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 = {$
+- 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])