vault backup: 2025-03-03 10:06:24

This commit is contained in:
Marco Realacci 2025-03-03 10:06:24 +01:00
parent 7e23b3a8d5
commit 70c554d9fa

View file

@ -154,4 +154,14 @@ lock(i) :=
unlock(i) :=
FLAG[i] <- down
return
```
```
**Features:**
- it satisfies MUTEX
- it satisfies bounded bypass, with bound = 1
- it requires 2 one-bit SRSW registers (the flags and 1 one-bit MRMW registers (AFTER_YOU)
- Each lock-unlock requires 5 accesses to the registers (4 for lock and 1 for unlock)
##### MUTEX proof
Assume p0 and p1 are simultaneously in the CS.
How has p0 entered its CS?