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

This commit is contained in:
Marco Realacci 2025-03-24 09:24:23 +01:00
parent 900d972834
commit 78d5af9cda

View file

@ -70,4 +70,26 @@ this implementation satisfies the three requirements for the splitter
A **timestamp generator** is a concurrent object that provides a single operation get_ts such that:
1. (*validity*) not two invocations of get_ts return the same value
2. (*consistency*) if one process terminates its invocation of get_ts before another one starts, the first receives a timestamp that is smaller than the one received by the second one
3. (*obstruction freedom*) if run in isolation
3. (*obstruction freedom*) if run in isolation, it eventually terminates
Idea: use something like a splitter for possible timestamp, so that only the process that receives S (if any) can get that timestamp.
We have:
- `DOOR[i]`: MRMW boolean atomic register initialized at 1, for all i
- `LAST[i]`: MRMW atomic register initialized at whatever process index, for all i
- NEXT: integer initialized at 1
```
get_ts(i) :=
k <- NEXT
while true do
LAST[k] <- i
if DOOR[k] = 1 then
DOOR[k] <- 0
if LAST[k] = i then
NEXT++
return k
k++
```
#### Soundness theorem (yes, again)
this implementation satisfies the three properties of the timestamp generator