diff --git a/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md b/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md index 8c5717c..c4288ee 100644 --- a/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md +++ b/Concurrent Systems/notes/8 - Enhancing Liveness Properties.md @@ -38,4 +38,12 @@ Let Q be the set of proc.'s that performed these invocations. - since crashed are fail-stop, eventually `NEED_HELP[j]` is no longer modified ($\forall j \not \in Q$) - $\exists \tau' \geq \tau$ where all proc.'s in Q compute the same X -**Observation:** \ No newline at end of file +**Observation:** $Q \subseteq X$ (it is possible that $p_j$ sets `NEED_HELP[j]` and then fails) + +By definition of $\Omega_{X}, \exists \tau'' \geq t'$ s.t. all proc.'s in Q have the same `ev_leader(X)` +- the leader belongs to Q, since it cannot be failed +- this is the only process allowed to proceed +- because run in isolation, it eventually terminates (because of obstruction freedom) + +#### On implementing $\Omega$ +It can be proved that there exists no wait-free implementation of $\Omega$ in an asynchronous \ No newline at end of file