marcorealacci/master-degree-notes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

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

Browse source
This commit is contained in:
Marco Realacci 2025-03-04 09:24:45 +01:00
parent bc5b4f5c16
commit c02aeb0bb1
1 changed files with 13 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
Concurrent Systems/notes/Lezione2.md
View file

@ -103,4 +103,16 @@ unlock(i) :=
###### Is it deadlock free?
Since DLF is deadlock free, it is sufficient to prove that at least one process invokes DLF.lock.
If TURN = k and $p_k$ invoked lock, then it finds TURN = k and exits its wait.
Otherwise, any other process will find `FLAG[TURN] = down` and
Otherwise, any other process will find `FLAG[TURN] = down` and exits from its wait.
**Lemma 1:** if TURN = i and `FLAG[i] = up` then $p_i$ enters the CS in at most n-1 iterations
Observation 1: TURN changes only when FLAG[i] is down (after pi has completed its CS)
Observation 2: FLAG[i] = up -> either pi is in its CS or pi is competing for its CS -> it eventually invokes (if not already) DLF.lock
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
- because of Observation 2, $i \in Y$
- because of Observation 3, once FLAG[i] is set, Y cannot grow anymore