diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index d0e5832..6e215b8 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -229,9 +229,9 @@ }, "active": "0d64f519fd7f9420", "lastOpenFiles": [ - "Concurrent Systems/slides/class 8.pdf", - "Concurrent Systems/notes/8 - Enhancing Liveness Properties.md", "Concurrent Systems/notes/7- MUTEX-free concurrency.md", + "Concurrent Systems/notes/8 - Enhancing Liveness Properties.md", + "Concurrent Systems/slides/class 8.pdf", "Concurrent Systems/slides/class 7.pdf", "Concurrent Systems/notes/6a - Alternatives to Atomicity.md", "Concurrent Systems/notes/3a - Hardware primitives & Lamport Bakery algorithm.md", diff --git a/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md b/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md index 8382670..2d325ee 100644 --- a/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md +++ b/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md @@ -103,5 +103,15 @@ We assume a weak timestamp generator, i.e. a function such that, if it returns a TS[1..n] : SWMR atomic R/W registers init at 0 need_help(i) := - TS[i] -``` \ No newline at end of file + TS[i] <- weak_ts() + repeat + competing <- {j : TS[j] != 0 and j ∉ suspected_i} + ⟨t,j⟩ <- min{⟨TS[x],x⟩ | x ∈ competing} + until j = i + +stop_help(i) := + TS[i] <- 0 +``` + +##### Theorem: +the contention manager just seen transforms an obstruction-free implementation into a wait-free enriched implementation. \ No newline at end of file