marcorealacci/master-degree-notes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

vault backup: 2025-03-25 15:32:22

Browse source
This commit is contained in:
Marco Realacci 2025-03-25 15:32:22 +01:00
parent 95d46b5797
commit 378c5252b2
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
Concurrent Systems/notes/8 - Enhancing Liveness Properties.md
View file

@ -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 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 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 ### From obstruction-freedom to non-blocking
``` ```
@ -25,7 +25,7 @@ need_help(i) :=
NEED_HELP[i] <- true NEED_HELP[i] <- true
repeat repeat
X <- {j : NEED_HELP[j]} 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) := stop_help(i) :=
NEED_HELP[i] <- false NEED_HELP[i] <- false