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

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

@@ -132,4 +132,7 @@ Since ⟨ti,i⟩ is the minimum index of a non-terminating invocation
 - 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$ )
+Since $p_i$ is correct, eventually (for all $p_k$ correct):
+- i will not be anymore in $suspected_{i}$ (as $p_i$ will not crash as its correct)
+- $⟨ti,i⟩ = min\{⟨TS[x],x⟩ \space|\space x \in competing_{k}\}$ (all pk will select pi as the minimum)
+Hence, the invocation with index ⟨ti,i⟩ will eventually have exclusive execution, and because of obstruction freedom it eventually terminates.