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

Concurrent Systems/notes/Lezione1.md

@@ -173,6 +173,12 @@ 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).
+- If the wait condition is true, then it wins (and waits 0).
 
-Otherwise, i
+- Otherwise, it must be that `FLAG[1] = UP` **AND** `AFTER_YOU = 0` (quindi p1 ha invocato il lock e p0 dovrà aspettare).
+
+- If p1 never locks anymore then p0 will eventually read `F[1]` and win (waiting 1).
+
+- It is possible tho that p1 locks again:
+	- if p0 reads `F[1]` before p1 locks, then p0 wins (waiting 1)
+	- otherwise p1 sets A_Y to 1 and suspends in its wait (`F[0] = up AND A_Y = 1`), p0 will eventually rea