vault backup: 2025-03-25 08:53:01

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:**