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

.obsidian/workspace.json

@@ -6,7 +6,7 @@
       {
         "id": "efd2410a71337f52",
         "type": "tabs",
-        "dimension": 85.67335243553008,
+        "dimension": 64.46991404011462,
         "children": [
           {
             "id": "383fb8ddbc7a9dc8",
@@ -42,7 +42,7 @@
       {
         "id": "496ffcebad48669d",
         "type": "tabs",
-        "dimension": 14.326647564469914,
+        "dimension": 35.53008595988539,
         "children": [
           {
             "id": "879210c00db77468",

Concurrent Systems/notes/8 - Enhancing Liveness Properties.md

@@ -36,8 +36,8 @@ stop_help(i) :=
 *Proof:*
 By contr., $\exists \tau$ s.t. $\exists$ many (> 0) op.'s invoked concurrently that never terminate.
 Let Q be the set of proc.'s that performed these invocations.
-- by enrichment, eventually `NEED_HELP[i]=T` ($\forall i\in Q$) forever
-- since crashed are fail-stop, eventually `NEED_HELP[j]` is no longer modified ($\forall j \not \in Q$)
+- by enrichment, eventually `NEED_HELP[i]=T` forever ($\forall i\in Q$)
+- since crashes 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:** $Q \subseteq X$ (it is possible that $p_j$ sets `NEED_HELP[j]` and then fails)