From 10447c9ab994f208f7e739262519222c6474119d Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 25 Mar 2025 17:12:22 +0100 Subject: [PATCH] vault backup: 2025-03-25 17:12:22 --- .obsidian/workspace.json | 8 ++++---- .../notes/8 - Enhancing Liveness Properties.md | 5 +++-- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index edfd9a0..d0e5832 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -6,7 +6,7 @@ { "id": "efd2410a71337f52", "type": "tabs", - "dimension": 64.46991404011462, + "dimension": 53.86819484240688, "children": [ { "id": "383fb8ddbc7a9dc8", @@ -42,7 +42,7 @@ { "id": "496ffcebad48669d", "type": "tabs", - "dimension": 35.53008595988539, + "dimension": 46.13180515759313, "children": [ { "id": "879210c00db77468", @@ -229,9 +229,9 @@ }, "active": "0d64f519fd7f9420", "lastOpenFiles": [ - "Concurrent Systems/notes/7- MUTEX-free concurrency.md", - "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/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 b34e53c..8382670 100644 --- a/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md +++ b/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md @@ -95,12 +95,13 @@ Forall i $\Omega_{X}$ is not stronger than ♢P (so, ♢P is strictly stronger) The formal proof consists in showing that if $\Omega_{X}$ was stronger than ♢P, then consensus would be possible in an asynchronous system with crashes and atomic R/W registers. -(because ♢P can solve consensus, ) +(because ♢P can be used to solve consensus) #### A contention manager for ♢P We assume a weak timestamp generator, i.e. a function such that, if it returns a positive value t to some process, only a finite number of invocations can obtain a timestamp smaller than or equal to t ``` TS[1..n] : SWMR atomic R/W registers init at 0 -... +need_help(i) := + TS[i] ``` \ No newline at end of file