marcorealacci/master-degree-notes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

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

Browse source
This commit is contained in:
Marco Realacci 2025-03-03 10:11:24 +01:00
parent 70c554d9fa
commit 11d3ba7399
4 changed files with 15 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

11
Concurrent Systems/notes/Lezione1.md
View file

@ -164,4 +164,15 @@ unlock(i) :=
##### MUTEX proof
Assume p0 and p1 are simultaneously in the CS.
How has p0 entered its CS?
a) `FLAG[1] = down`, this is possible only with the following interleaving:
![[Pasted image 20250303100721.png]]
b) `AFTER_YOU = 1`, this is possible only with the following interleaving:
![[Pasted image 20250303100953.png]]
##### Bounded Bypass proof (with bound = 1)
If the wait condition is true, then it wins (and waits 0).
Otherwise, i