vault backup: 2025-03-04 09:29:45

This commit is contained in:
Marco Realacci 2025-03-04 09:29:45 +01:00
parent c02aeb0bb1
commit 5136e40d3e

View file

@ -113,6 +113,12 @@ Observation 2: FLAG[i] = up -> either pi is in its CS or pi is competing for its
Observation 3: if $p_j$ invokes lock after that FLAG[i] is set, $p_j$ blocks in its wait
Let Y be the set of processes competing for the CS
Let Y be the set of processes competing for the CS (suspended on the DLF.lock)
- because of Observation 2, $i \in Y$
- because of Observation 3, once FLAG[i] is set, Y cannot grow anymore
- because DLF is deadlock free, eventually one $p_{y} \in Y$ wins if $y = i$.
- if $y = i$ we are done
- otherwise, Y shrinks by one. And because of Observation 1, TURN and FLAG[TURN] don't change, so $p_y$ cannot enter Y again.
- Iterating this reasoning we can see that $p_i$ will eventually win, and the worst case is when is the last winner.
**Lemma 2:** If FLAG[i] = up, then TURN is set to i in at most $(n-1)^2$