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

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

View file

@ -90,9 +90,10 @@ unlock(i) :=
FLAG[i] <- 0 FLAG[i] <- 0
return return
``` ```
We say that: We say that: $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$
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$
>[!info] What is the `wait` condition actually checking?
>In the wait condition we check that all other processes are at a lower level.
##### 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