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