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

vault backup: 2025-03-25 18:22:22

Browse source
This commit is contained in:
Marco Realacci 2025-03-25 18:22:22 +01:00
parent 5b2ab98e5b
commit a1eb088190
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -136,3 +136,7 @@ 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) - 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) - $⟨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. Hence, the invocation with index ⟨ti,i⟩ will eventually have exclusive execution, and because of obstruction freedom it eventually terminates.
#### On implementing ♢P
- every non-failed process has eventually an upper bound on the write delay
- by properly setting timers, eventually crashed processes are distinguished from the non-crashed ones by looking at the suspicions: for the crashed ones, this numbers increases indefinitely; for non-crashed ones, some reset eventually happens.