From bd2fd04d6c0626fd64107d94e9eb98dfb95b5c82 Mon Sep 17 00:00:00 2001
From: Marco Realacci <marco@marcorealacci.me>
Date: Tue, 25 Mar 2025 18:07:22 +0100
Subject: [PATCH] vault backup: 2025-03-25 18:07:22

---
 .obsidian/workspace.json                              | 11 ++++++-----
 .../notes/8 - Enhancing Liveness Properties.md        | 11 ++++++++++-
 2 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index ffb99c8..e70583e 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -14,12 +14,12 @@
             "state": {
               "type": "markdown",
               "state": {
-                "file": "Concurrent Systems/notes/1b - Peterson algorithm.md",
+                "file": "Concurrent Systems/notes/8 - Enhancing Liveness Properties.md",
                 "mode": "source",
                 "source": false
               },
               "icon": "lucide-file",
-              "title": "1b - Peterson algorithm"
+              "title": "8 - Enhancing Liveness Properties"
             }
           }
         ]
@@ -98,7 +98,8 @@
       }
     ],
     "direction": "horizontal",
-    "width": 307.5
+    "width": 307.5,
+    "collapsed": true
   },
   "right": {
     "id": "bc4b945ded1926e3",
@@ -212,12 +213,12 @@
   },
   "active": "383fb8ddbc7a9dc8",
   "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/1b - Peterson algorithm.md",
     "Concurrent Systems/notes/2b - Round Robin algorithm.md",
     "Concurrent Systems/notes/2 - Fast mutex by Lamport.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 2d325ee..92b587f 100644
--- a/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md	
+++ b/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md	
@@ -114,4 +114,13 @@ stop_help(i) :=
 ```
 
 ##### Theorem:
-the contention manager just seen transforms an obstruction-free implementation into a wait-free enriched implementation.
\ No newline at end of file
+the contention manager just seen transforms an obstruction-free implementation into a wait-free enriched implementation.
+
+*Proof:*
+By contradiction, $\exists$ an invocation of a correct $p_i$ that never terminates.
+Let $ti$ be its timestamp.
+- choose the minimum of such ⟨ti,i⟩
+
+By constraint of weak_ts(), the set of invocations smaller than ⟨ti,i⟩ (call it I) is finite
+- for every invocation ∈ I from a process $p_j$ that crashed during its execution
+	- $p_i$ will eventually and forever suspect $p_j$ (i.e. j ∈ `suspected_i`)
\ No newline at end of file