From 5b2ab98e5b679d8da0bd44a837f9086afd295dae Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 25 Mar 2025 18:17:22 +0100 Subject: [PATCH] vault backup: 2025-03-25 18:17:22 --- .../notes/8 - Enhancing Liveness Properties.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md b/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md index 9cd1ca9..ce2a03f 100644 --- a/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md +++ b/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$ ) \ No newline at end of file +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. \ No newline at end of file