vault backup: 2025-03-10 22:23:12

This commit is contained in:
Marco Realacci 2025-03-10 22:23:12 +01:00
parent a67c8416a2
commit 0982714f83

View file

@ -80,3 +80,14 @@ unlock(i) :=
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! 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
```