vault backup: 2025-03-25 18:07:22

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.
+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`)