From 78d5af9cda3f9b249369841a5e90730b2dbaa72a Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 24 Mar 2025 09:24:23 +0100 Subject: [PATCH] vault backup: 2025-03-24 09:24:23 --- .../notes/7- MUTEX-free concurrency.md | 24 ++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/7- MUTEX-free concurrency.md b/Concurrent Systems/notes/7- MUTEX-free concurrency.md index 3eafc60..09dd627 100644 --- a/Concurrent Systems/notes/7- MUTEX-free concurrency.md +++ b/Concurrent Systems/notes/7- MUTEX-free concurrency.md @@ -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 \ No newline at end of file