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