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

Concurrent Systems/notes/8 - Enhancing Liveness Properties.md

@@ -123,4 +123,13 @@ Let $ti$ be its timestamp.
 
 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`)
+	- $p_i$ will eventually and forever suspect $p_j$ (i.e. j ∈ `suspected_i`)
+	- eventually j will not be anymore in completing
+		- $p_{j}$ will not anymore prevent $p_i$ from proceeding
+
+Since ⟨ti,i⟩ is the minimum index of a non-terminating invocation
+- all invocations in I of correct processes terminate
+- if such processes invoke need_help() again, they obtain greater indexes
+- eventually I gets emptied
+
+Since $p_i$ is correct, eventually (for all $p_k$ )