From 378c5252b22462656f65f8a87d79b895af8244fc Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 25 Mar 2025 15:32:22 +0100 Subject: [PATCH] vault backup: 2025-03-25 15:32:22 --- Concurrent Systems/notes/8 - Enhancing Liveness Properties.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md b/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md index 4e59d5b..d13cbb3 100644 --- a/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md +++ b/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md @@ -15,7 +15,7 @@ Can we take the most basic protocol that satisfies the most basic liveness prope 1. *(Validity)* `ev_leader(x)` always contains a process ID 2. *(Eventual leadership)* eventually, all `ev_leader(X)` of all non-crashed processes of X for ever contain the same process ID, that is one of them -REMARK: the moment in which all variables contain the same leader is unknown +REMARK: the moment in which all variables contain the same leader is unknown. ### From obstruction-freedom to non-blocking ``` @@ -25,7 +25,7 @@ need_help(i) := NEED_HELP[i] <- true repeat X <- {j : NEED_HELP[j]} - until ev_leader(X) = i + until ev_leader(X) = i # loopa finché ev_leader non uguale per tutti stop_help(i) := NEED_HELP[i] <- false