197 lines
No EOL
6.3 KiB
Markdown
197 lines
No EOL
6.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$.
|
|
|
|
**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 ...
|
|
continuare
|
|
|
|
**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⟩$$
|
|
|
|
#### 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 pi and pj competing for the CS and pj wins
|
|
|
|
Then, pj enters its CS, completes it, unlocks and then invokes lock again
|
|
- If pi has entered the CS, √
|
|
- Otherwise, by Lemma1, MY_TURN[i] < MY_TURN[j], then pj cannot bypass pi 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) |