vault backup: 2025-03-08 18:11:57

This commit is contained in:
Marco Realacci 2025-03-08 18:11:57 +01:00
parent 3645c0f6f4
commit 60cff73ec8

View file

@ -48,9 +48,10 @@ unlock(i) :=
- Each lock-unlock requires 5 accesses to the registers (4 for lock and 1 for unlock) - Each lock-unlock requires 5 accesses to the registers (4 for lock and 1 for unlock)
##### MUTEX proof ##### MUTEX proof
Assume p0 and p1 are simultaneously in the CS. >[!info]
>Remember that, in the [[#Correct solution|correct implementation]], there is this line: `wait (FLAG[1-i] = down OR AFTER_YOU != i)`. Thus, to access the critical section (the `return` instruction of the `lock` function), the possibilities are just the two discussed above.
How has p0 entered its CS? **How has p0 entered its CS?**
a) `FLAG[1] = down`, this is possible only with the following interleaving: a) `FLAG[1] = down`, this is possible only with the following interleaving:
![[Pasted image 20250303100721.png]] ![[Pasted image 20250303100721.png]]
@ -89,7 +90,8 @@ unlock(i) :=
FLAG[i] <- 0 FLAG[i] <- 0
return return
``` ```
We say that pi is at level h when it exits from the h-th wait -> a process at level h is at any level <= h We say that:
if $p_i$ is at level $h$ when it exits from the $h$-th wait $\to$ a process at level $h$ is at any level $<= h$
##### MUTEX proof ##### MUTEX proof
Lemma: for every $ \in \{0,\dots,n-1\}$ , at most n- processes are at level , this implies MUTEX by taking = n-1 Lemma: for every $ \in \{0,\dots,n-1\}$ , at most n- processes are at level , this implies MUTEX by taking = n-1