vault backup: 2025-03-10 23:37:52

This commit is contained in:
Marco Realacci 2025-03-10 23:37:52 +01:00
parent 367d22ad37
commit bd349a41c2

View file

@ -77,21 +77,11 @@ unlock(i) :=
STAGE[i] <- 0
FLAG[i] <- down
```
Since the LOCK is like before, the revised protocol satisfies MUTEX. Furthermore, you can prove that it satisfies bounded bypass with bound n-1 -> EXERCISE!
Let's remember ourselves how is the locking function defined:
```
lock(i) :=
FLAG[i] <- up
repeat
STAGE[i] <- 0
wait (foreach j != i, FLAG[j] = down OR DATE[i] < DATE[j])
STAGE[i] <- 1
until foreach j != i, STAGE[j] = 0
```
>[!note] let's remember ourselves [[### Aravinds algorithm|the locking function]]
(a causa di un bug di Obsidian, se non vedi la dimostrazione)
(a causa di un bug, riavvia Obsidian se non vedi la dimostrazione qui sotto)
>[!question]- mostra mia soluzione
>- $p_n$ invokes lock alone, completes its CS and so `DATE[n] = n`
>- then as DATE is either set to n or decreased, for each i, `DATE[i] < n`