vault backup: 2025-03-03 10:31:24

Concurrent Systems/notes/Lezione1.md

@@ -206,4 +206,15 @@ unlock(i) :=
 ```
 We say that pi is at level h when it exits from the h-th wait -> a process at level h is at any level <= h
 
-##### MUTE
+##### MUTEX proof
+Lemma: for every $ℓ \in \{0,\dots,n-1\}$ , at most n-ℓ processes are at level ℓ, this implies MUTEX by taking ℓ = n-1
+
+Proof by induction on ℓ
+
+Base (ℓ=0): trivial
+
+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