277 lines
9.3 KiB
Markdown
277 lines
9.3 KiB
Markdown
|
||
### Hardware primitives
|
||
Atomic R/W registers provide quite a basic computational model.
|
||
|
||
We can strenghten the model by adding specialized HW primitives, that essentially perform in an atomic way the combination of some atomic instructions.
|
||
Usually, every operating system provides at least one specilized HW primitive.
|
||
|
||
##### Most common ones:
|
||
- **Test&set:** atomic read+write of a boolean register
|
||
- **Swap:** atomic read+write of a general register (generalization of the above)
|
||
- **Fetch&add:** atomic read+increase of an integer register
|
||
- **Compare&swap:** tests the value of a general register, returns a boolean (result of the comparison, true if it is the same).
|
||
|
||
#### Test&Set
|
||
```
|
||
Let X be a boolean register
|
||
|
||
X.test&set() :=
|
||
tmp <- X
|
||
X <- 1
|
||
return tmp
|
||
|
||
(the function is implemented in an atomic way by the hardware by suspending the interruptions!)
|
||
```
|
||
|
||
###### How do we use it for MUTEX?
|
||
```
|
||
lock() :=
|
||
wait X.test&set() = 0
|
||
return
|
||
|
||
|
||
unlock() :=
|
||
X <- 0
|
||
return
|
||
```
|
||
|
||
|
||
#### Swap
|
||
```
|
||
X general register
|
||
|
||
X.swap(v) :=
|
||
tmp <- X
|
||
X <- v
|
||
return tmp
|
||
```
|
||
|
||
###### How do we use it for MUTEX?
|
||
```
|
||
lock() :=
|
||
wait X.swap(1) = 0
|
||
return
|
||
|
||
unlock() :=
|
||
X <- 0
|
||
return
|
||
```
|
||
|
||
#### Compare&swap
|
||
```
|
||
X boolean register
|
||
|
||
X.compare&swap(old, new) :=
|
||
if X = old then
|
||
X <- new
|
||
return true
|
||
return false
|
||
```
|
||
###### How do we use it for MUTEX?
|
||
```
|
||
Initialize X at 0
|
||
|
||
lock() :=
|
||
wait X.compare&swap(0, 1) = true
|
||
return
|
||
|
||
unlock() :=
|
||
X <- 0
|
||
return
|
||
```
|
||
|
||
#### Fetch&add
|
||
Up to now, all solutions enjoy deadlock freedom, but allow for starvation. So let's use Round Robin to promote the liveness property!
|
||
|
||
Let X be an integer register; the Fetch&add primitive is implemented as follows:
|
||
```
|
||
X.fetch&add(v) :=
|
||
tmp <- X
|
||
X <- X+v
|
||
return tmp
|
||
```
|
||
|
||
###### How do we use it for MUTEX?
|
||
```
|
||
Initialize TICKET and NEXT at 0
|
||
|
||
lock() :=
|
||
my_ticket <- TICKET.fetch&add(1)
|
||
wait my_ticket = NEXT
|
||
return
|
||
|
||
unlock() :=
|
||
NEXT <- NEXT + 1
|
||
return
|
||
```
|
||
|
||
>[!note] a>It is bounded bypass with bound n-1>
|
||
|
||
### Safe registers
|
||
Atomic R/W and specialized HW primitives provide some form of atomicity. But is it possible to enforce MUTEX without atomicity?
|
||
|
||
A **MRSW Safe register** is a register that provides READ and WRITE such that:
|
||
1. every READ that does not overlap with a WRITE returns the value stored in the register
|
||
2. a READ that overlaps with a WRITE can return **any possible value** (of the register domain).
|
||
|
||
A **MRMW Safe register** behaves like a MRSW safe register, when WRITE operations do not overlap. Otherwise, in case of overlapping WRITEs, the register can contain any value (of the register domain).
|
||
*(Ci sta comunque lo stesso problema)*
|
||
|
||
> Si chiama safe nel senso che se ci sono letture overlapping siamo safe. Ma è letteralmente l'unica cosa safe che abbiamo!
|
||
|
||
This is the weakest type of register that is useful in concurrency.
|
||
|
||
### Bakery Algorithm
|
||
**The idea is that**
|
||
- every process gets a ticket
|
||
- because we don't have atomicity, tickets may be not unique
|
||
- tickets can be made unique by pairing them with the process ID
|
||
- the smallest ticket (seen as a pair) grants the access to the CS
|
||
|
||
```
|
||
Initialize FLAG[i] to down and MY_TURN[i] to 0, for all i
|
||
|
||
lock(i) :=
|
||
FLAG[i] <- up
|
||
MY_TURN[i] <- max{MY_TURN[1],...,MY_TURN[n]}+1
|
||
FLAG[i] <- down
|
||
forall j != i
|
||
wait FLAG[j] = down
|
||
wait (MY_TURN[j] = 0 OR ⟨MY_TURN[i],i⟩ < ⟨MY_TURN[j],j⟩)
|
||
|
||
unlock(i) :=
|
||
MY_TURN[i] <- 0
|
||
```
|
||
Se il ticket number è minore si ottiene l'accesso, se il ticket number è uguale, allora si vede il process ID minore.
|
||
|
||
> It is possible that while reading, other processes are writing their turn! So it's possible that I read something unpredictable! We need to consider it in the proofs.
|
||
|
||
###### Why is the flag needed?
|
||
Without it, if two process $i$ and $j$ sets MY_TURN at the same time, then $i$ goes to sleep, $j$ enters the CS, but when $i$ wakes up, it will enter too!
|
||
|
||
#### MUTEX proof
|
||
**Lemma 1:** if $p_i$ enters the bakery before $p_j$, then `MY_TURN[i] < MY_TURN[j]`.
|
||
|
||
*Proof:*
|
||
- let t be the value of `MY_TURN[i]` after $p_{i}$ exits the doorway (after flag <- down)
|
||
- when $p_j$ computes its ticket, it reads $t$ from `MY_TURN[i]`, it reads t from `MY_TURN[i]` (no write overlapping with this read)
|
||
- Hence, `MY_TURN[j]` is at least $t+1$. (legge correttamente almeno t, gli altri boh ma non ci interessa ora)
|
||
|
||
**Lemma 2:** Let $p_i$ be in the CS and $p_j$ is in the doorway or in the bakery; then, $$⟨MY\_TURN[i] , i⟩ < ⟨MY\_TURN[j] , j⟩$$*Proof:*
|
||
If $p_i$ is in the CS, it has terminated its first wait for $j$
|
||
let's consider the read of `FLAG[j]` done by $p_i$ that terminates such wait
|
||
|
||
W.r.t. the execution of $p_j$, it can be that
|
||
- this read overlaps with `FLAG[j] <- up` by Lemma 1, `MY_TURN[i] < MY_TURN[j]` and ok
|
||
- this read is contained within the computation of `MY_TURN[j]`, but it's not possible, since `MY_TURN` is computed with the `FLAG` up
|
||
- this read overlaps with `FLAG[j] <- down` or this read happens when $p_j$ is in the bakery:
|
||
- `MY_TURN[j]` has been decided and no write will change it until $p_j$ is in the bakery, and `MY_TURN[j] > 0` of course
|
||
- When $p_i$ evaluated the second wait for j, it found out that $⟨MY_TURN[i],i⟩ < ⟨MY_TURN[j],j⟩$, good!
|
||
|
||
**MUTEX:** $p_i$ and $p_j$ cannot simultaneously be in the CS:
|
||
*Proof:*
|
||
By contradiction, by Lemma 2 applied twice, we would have:
|
||
$$⟨MY\_TURN[i] , i⟩ < ⟨MY\_TURN[j] , j⟩ \land ⟨MY\_TURN[j] , j⟩ < ⟨MY\_TURN[i] , i⟩$$
|
||
Which is of course not possible, how in the world is it possible that x < y and y < x at the same time? √
|
||
|
||
#### Deadlock freedom proof
|
||
By contradiction, assume that there is a lock but nobody enters its CS
|
||
- All processes in the bakery (we will call this set Q) are blocked in their wait
|
||
- The first wait cannot block forever
|
||
- All $p_i \in Q$ have their FLAG down
|
||
- All $p_i \not \in Q$ have their FLAG down (if not in the doorway) or will eventually put their FLAG down (cannot remain in the doorway forever)
|
||
- The second wait cannot block all of them forever
|
||
- Tickets can be totally ordered (lexicographically)
|
||
- Let `<MY_TURN[i], j>` be the minimun
|
||
- The second wait evaluated by $p_i$ eventually succeeds for all j
|
||
- if $p_j$ is before the doorway, then `MY_TURN[j] = 0`
|
||
- if $p_{j}$ is in the doorway, then `MY_TURN[i] < MY_TURN[j]` (bc of Lemma 1)
|
||
- 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)
|
||
Let $p_i$ and $p_j$ competing for the CS and $p_j$ wins
|
||
|
||
Then, $p_j$ enters its CS, completes it, unlocks and then invokes lock again
|
||
- If $p_i$ has entered the CS, √
|
||
- 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
|
||
- (indeed, since there is no deadlock, when pi is waiting somebody enters the CS)
|
||
|
||
### Aravind’s algorithm
|
||
Problem with Lamport's algorithm: registers must be unbounded (every invocation of lock potentially increases the counter by 1 -> domain of the registers is all natural numbers!)
|
||
|
||
For all processes, we have a FLAG and a STAGE (both binary MRSW) and a DATE (MRMW) register that ranges from 1 to 2n.
|
||
|
||
```
|
||
For all i, initialize
|
||
FLAG[i] to down
|
||
STAGE[i] to 0
|
||
DATE[i] to i
|
||
|
||
lock(i) :=
|
||
FLAG[i] <- up
|
||
repeat
|
||
STAGE[i] <- 0
|
||
wait (foreach j != i, FLAG[j] = down OR DATE[i] < DATE[j])
|
||
STAGE[i] <- 1
|
||
until foreach j != i, STAGE[j] = 0
|
||
|
||
unlock(i) :=
|
||
tmp <- max_j{DATE[j]}+1
|
||
if tmp >= 2n
|
||
then foreach j, DATE[j] <- j
|
||
else DATE[i] <- tmp
|
||
STAGE[i] <- 0
|
||
FLAG[i] <- down
|
||
```
|
||
|
||
#### MUTEX proof
|
||
**Theorem:** if $p_i$ is in the CS, then $p_j$ cannot simultaneously be in the CS.
|
||
*Proof:* by contradiction.
|
||
|
||
Let's consider the execution of $p_i$ leading to its CS:
|
||
![[Pasted image 20250310172134.png]]
|
||
|
||
**Corollary** (of the MUTEX proof)**:** DATE is never written concurrently.
|
||
|
||
#### Bounded bypass proof
|
||
**Lemma 1:** exactly after n CSs there is a reset of DATE.
|
||
*Proof:*
|
||
- the first CS leads $max_j{DATE[j]}$ to n+1
|
||
- the seconds CS leads ... to n+2
|
||
- ...
|
||
- the n-th read leads ... to n+n = 2n -> RESET
|
||
|
||
**Lemma 2:** there can be at most one reset of DATE during an invocation of a lock
|
||
*Proof:*
|
||
- let $p_i$ invoke lock, if no reset occurs, ok
|
||
- otherwise, let us consider the moment in which a reset occurs
|
||
- 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]$
|
||
- $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)
|
||
- all $p_{1}\dots p_{n}$ surpass $p_{n}$
|
||
- then $p_n$ enters and it resets the DATE in its unlock
|
||
- only 1 reset and it is the worst case!
|
||
|
||
**Theorem:** the algorithm satisfies bounded bypass with bound $2n-2$.
|
||
*Proof:*
|
||
![[Pasted image 20250310103703.png]]
|
||
so by this, the very worst possible case is that my lock experiences that.
|
||
|
||
It looks like I can experience at most $2n-1$ other critical sections, but it is even better, let's see:
|
||
- $p_n$ invokes lock alone, completes its CS (the first after the reset) and its new DATE is n+1
|
||
- all processes invoke lock simultaneously
|
||
|
||
|
||
#### Improvement of Aravind’s algorithm
|
||
```
|
||
unlock(i) :=
|
||
∀j≠i.if DATE[j] > DATE[i] then
|
||
DATE[j] <- DATE[j]-1
|
||
DATE[i] <- n STAGE[i] <- 0
|
||
FLAG[i] <- down
|
||
```
|
||
|
||
Since the LOCK is like before, the revised protocol satisfies MUTEX. Furthermore, you can prove that it satisfies bounded bypass with bound n-1 -> EXERCISE!
|
||
|