vault backup: 2025-03-10 17:30:21

This commit is contained in:
Marco Realacci 2025-03-10 17:30:21 +01:00
parent 0f9edce76b
commit f6767fc58b

View file

@ -232,6 +232,7 @@ unlock(i) :=
Let's consider the execution of $p_i$ leading to its CS: Let's consider the execution of $p_i$ leading to its CS:
![[Pasted image 20250310172134.png]] ![[Pasted image 20250310172134.png]]
**Corollary** (of the MUTEX proof)**:** DATE is never written concurrently.
#### Bounded bypass proof #### Bounded bypass proof
**Lemma 1:** exactly after n CSs there is a reset of DATE. **Lemma 1:** exactly after n CSs there is a reset of DATE.
@ -246,7 +247,7 @@ Let's consider the execution of $p_i$ leading to its CS:
- let $p_i$ invoke lock, if no reset occurs, ok - let $p_i$ invoke lock, if no reset occurs, ok
- otherwise, let us consider the moment in which a reset occurs - otherwise, let us consider the moment in which a reset occurs
- if pi is the next process that enters the CS, ok - if pi is the next process that enters the CS, ok
- Otherwise let $p_j$ be the process that enters, its next date is $n+1 > DATE[i]$ - Otherwise let $p_j$ be the process that enters; its next date is $n+1 > DATE[i]$
- $p_{j}$ cannot surpass $p_i$ again (before a RESET) - $p_{j}$ cannot surpass $p_i$ again (before a RESET)
- The worst case is then all processes perform lock together and $i = n$ (i am process n) - The worst case is then all processes perform lock together and $i = n$ (i am process n)
- all $p_{1}\dots p_{n}$ surpass $p_{n}$ - all $p_{1}\dots p_{n}$ surpass $p_{n}$