vault backup: 2025-03-10 09:45:11

This commit is contained in:
Marco Realacci 2025-03-10 09:45:11 +01:00
parent 8d09674312
commit 5db269c6a1
2 changed files with 18 additions and 3 deletions

View file

@ -34,9 +34,9 @@
"type": "pdf",
"state": {
"file": "Concurrent Systems/slides/class 3.pdf",
"page": 9,
"page": 10,
"left": -26,
"top": 276,
"top": 603,
"zoom": 0.57541567695962
},
"icon": "lucide-file-text",

View file

@ -163,4 +163,19 @@ If $p_i$ is in the CS, it has terminated its first wait for $j$
W.r.t. the execution of $p_j$, it can be that
- this read overlaps with `FLAG[j] <- up` by Lemma 1, `MY_TURN[i] < MY_TURN[j]` and ok
- this read is contained within the computation of `MY_TURN[j]`, but it's not possible, since `MY_TURN` is computed with the
- this read is contained within the computation of `MY_TURN[j]`, but it's not possible, since `MY_TURN` is computed with the `FLAG` up
- this read overlaps with `FLAG[j] <- down` or this read happens when $p_j$ is in the bakery:
- `MY_TURN[j] has been ...
continuare
**MUTEX:** $p_i$ and $p_j$ cannot simultaneously be in the CS:
*Proof:*
By contradiction, by Lemma 2 applied twice, we would have:
$$⟨MY\_TURN[i] , i⟩ < ⟨MY\_TURN[j] , j⟩ \land ⟨MY\_TURN[j] , j⟩ < ⟨MY\_TURN[i] , i⟩$$
#### Deadlock freedom proof
By contradiction, assume that there is a lock but nobody enters its CS
- All processes in the bakery (we will call this set Q) are blocked in their wait
- The first wait cannot block forever
- All $p_i \in Q$ have their FLAG down
- All $p_i \not \in Q$ have their FLAG down