From 304e5d401c27447a267301f9356c06cb32c23e18 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 25 Mar 2025 08:53:01 +0100 Subject: [PATCH] vault backup: 2025-03-25 08:53:01 --- .obsidian/workspace.json | 4 ++-- .../notes/8 - Enhancing Liveness Properties.md | 10 ++++++++++ 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index fe21334..e1d54a9 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -229,10 +229,10 @@ "companion:Toggle completion": false } }, - "active": "879210c00db77468", + "active": "0d64f519fd7f9420", "lastOpenFiles": [ - "Concurrent Systems/notes/8 - Enhancing Liveness Properties.md", "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/images/Pasted image 20250324091452.png", "Concurrent Systems/slides/class 7.pdf", diff --git a/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md b/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md index 6e2f97a..8c5717c 100644 --- a/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md +++ b/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md @@ -29,3 +29,13 @@ stop_help(i) := NEED_HELP[i] <- false ``` +**Theorem:** the contention manager just seen transforms an obstr.-free implementation into a non-blocking enriched implementation. + +*Proof:* +By contr., $\exists \tau$ s.t. $\exists$ many (> 0) op.'s invoked concurrently that never terminate. +Let Q be the set of proc.'s that performed these invocations. +- by enrichment, eventually `NEED_HELP[i]=T` ($\forall i\in Q$) forever +- since crashed are fail-stop, eventually `NEED_HELP[j]` is no longer modified ($\forall j \not \in Q$) + - $\exists \tau' \geq \tau$ where all proc.'s in Q compute the same X + +**Observation:** \ No newline at end of file