vault backup: 2025-03-24 09:09:23

This commit is contained in:
Marco Realacci 2025-03-24 09:09:23 +01:00
parent d73fe86372
commit 952b65725b

View file

@ -21,5 +21,35 @@ We have four new liveness properties
### A wait-free Splitter
Assume we have atomic R/W registers.
A **splitter** is a concurrent object that provides a single operation dir such that:
1. (*validity*)
A **splitter** is a concurrent object that provides a single operation **dir** such that:
1. (*validity*) it returns L, R or S (left, right, stop)
2. (*concurrency*) in case of n simultaneous invocations of **dir**
1. at most n-1 L are returned
2. at most n-1 R are returned
3. at most 1 S is returned
3. (*wait freedom*) it eventually terminates.
Idea:
- not all processes obtain the same value
- in a solo execution (i.e., without concurrency) the invoking process must stop (0 L && 0 R && at most 1 S)
We have:
- DOOR: MRMW boolean atomic register initialized at 1
- LAST: MRMW atomic register initialized at whatever process index
```
dir(i) :=
LAST <- i
if DOOR = 0 then
retunr R
else
DOOR <- 0
if LAST = i then
return S
else
return L
```
With 2 processes, we can have:
- one goes left and one goes right
- one goes left and the other stops
- one goes right and the other stops