vault backup: 2025-03-04 08:39:45

This commit is contained in:
Marco Realacci 2025-03-04 08:39:45 +01:00
parent 4a23786582
commit 9f90efacac

View file

@ -24,3 +24,21 @@ lock(i) :=
Problems: Problems:
- we don't want the FAIL - we don't want the FAIL
- it is possible to have an execution where nobody accesses its CS, if repeated forever it entails a deadlock - it is possible to have an execution where nobody accesses its CS, if repeated forever it entails a deadlock
```
Initialize Y at ⊥, X at any value (e.g., 0)
lock(i) :=
* FLAG[i] <- up
X <- i
if Y ≠ ⊥ then FLAG[i] <- down
wait Y = ⊥
goto *
else Y <- i
if X = i then return
else FLAG[i] <- down
∀j.wait FLAG[j] = down
if Y = i then return
else wait Y = 1
goto *