vault backup: 2025-03-10 11:51:08

This commit is contained in:
Marco Realacci 2025-03-10 11:51:08 +01:00
parent 6dd6dff2f6
commit 3e4f6d9195

View file

@ -188,11 +188,11 @@ By contradiction, assume that there is a lock but nobody enters its CS
- if $p_j$ is in the bakery, by assumption `⟨MY_TURN[i] , i⟩ < ⟨MY_TURN[j] , j⟩` since it is the minimum. - if $p_j$ is in the bakery, by assumption `⟨MY_TURN[i] , i⟩ < ⟨MY_TURN[j] , j⟩` since it is the minimum.
#### Bounded bypass proof (bound n-1) #### Bounded bypass proof (bound n-1)
Let pi and pj competing for the CS and pj wins Let $p_i$ and $p_i$ competing for the CS and $p_j$ wins
Then, pj enters its CS, completes it, unlocks and then invokes lock again Then, $p_j$ enters its CS, completes it, unlocks and then invokes lock again
- If pi has entered the CS, √ - If $p_j$ has entered the CS, √
- Otherwise, by Lemma1, $MY_TURN[i] < MY_TURN[j], then pj cannot bypass pi again! - Otherwise, by Lemma1, $MY\_TURN[i] < MY\_TURN[j]$, then $p_j$ cannot bypass $p_i$ again!
- At worse, pi has to wait all other proceeses before entering its CS - At worse, pi has to wait all other proceeses before entering its CS
- (indeed, since there is no deadlock, when pi is waiting somebody enters the CS) - (indeed, since there is no deadlock, when pi is waiting somebody enters the CS)