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

This commit is contained in:
Marco Realacci 2025-03-04 09:19:45 +01:00
parent 2941b894b0
commit bc5b4f5c16

View file

@ -100,4 +100,7 @@ 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