vault backup: 2025-03-10 16:45:21

This commit is contained in:
Marco Realacci 2025-03-10 16:45:21 +01:00
parent a7d26d90b7
commit 44a201686b

View file

@ -155,7 +155,7 @@ Without it, if two process $i$ and $j$ sets MY_TURN at the same time, then $i$ g
*Proof:*
- let t be the value of `MY_TURN[i]` after $p_{i}$ exits the doorway (after flag <- down)
- when $p_j$ computes its ticket, it reads $t$ from `MY_TURN[i]`, it reads t from `MY_TURN[i]` (no write overlapping with this read)
- Hence, `MY_TURN[j]` is at least $t+1$.
- Hence, `MY_TURN[j]` is at least $t+1$. (legge correttamente almeno t, gli altri boh ma non ci interessa ora)
**Lemma 2:** Let $p_i$ be in the CS and $p_j$ is in the doorway or in the bakery; then, $$⟨MY\_TURN[i] , i⟩ < ⟨MY\_TURN[j] , j⟩$$*Proof:*
If $p_i$ is in the CS, it has terminated its first wait for $j$