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

Concurrent Systems/notes/Lezione1.md

@@ -217,6 +217,11 @@ Induction (true for ℓ, to be proved for ℓ+1):
 - p at level ℓ can increase its level by writing its FLAG at ℓ+1 and its index in $A_Y[ℓ+1]$
 - let $p_x$ be the last one that writes `A_Y[ℓ+1]`, so `A_Y[ℓ+1]=x`
 - for $p_x$ to pass at level ℓ+1, it must be that $∀k≠x. F[k] < ℓ+1$, then $p_x$ is the only proc at level ℓ+1 and the thesis holds, since 1<=n-ℓ-1
-- otherwise, $p_x$ is blocked in the wait and so we have at most n-ℓ-1 processes at level ℓ+1 (i.e., those at level ℓ, that by induction are at most n-ℓ, except for px that is blocked in its (ℓ+1)-th wait).
+- otherwise, $p_x$ is blocked in the wait and so we have at most n-ℓ-1 processes at level ℓ+1: those at level ℓ, that by induction are at most n-ℓ, except for px that is blocked in its wait.
 
 ##### Starvation freedom proof
+**Lemma:** every process at level ℓ ($\leq n-1$) eventually wins $\to$ starvation freedom holds by taking $ℓ=0$.
+
+Reverse induction on ℓ
+Base ($ℓ=n-1$): trivial
+