vault backup: 2025-03-10 09:40:11

.obsidian/workspace.json

@@ -34,9 +34,9 @@
               "type": "pdf",
               "state": {
                 "file": "Concurrent Systems/slides/class 3.pdf",
-                "page": 7,
+                "page": 9,
                 "left": -26,
-                "top": 213,
+                "top": 276,
                 "zoom": 0.57541567695962
               },
               "icon": "lucide-file-text",
@@ -218,10 +218,10 @@
   },
   "active": "6edd4157a160e462",
   "lastOpenFiles": [
+    "Concurrent Systems/slides/class 3.pdf",
+    "Concurrent Systems/notes/3.md",
     "Concurrent Systems/notes/1 - CS Basics.md",
     "Concurrent Systems/notes/1 - CS Basics2.md",
-    "Concurrent Systems/notes/3.md",
-    "Concurrent Systems/slides/class 3.pdf",
     "Concurrent Systems/notes/2b - Round Robin algorithm.md",
     "Concurrent Systems/notes/2 - Fast mutex by Lamport.md",
     "Concurrent Systems/notes/1b - Peterson algorithm.md",
@@ -263,7 +263,6 @@
     "Biometric Systems/frequently asked questions/BS_questions.txt.md",
     "Biometric Systems/notes/9. Ear recognition.md",
     "Biometric Systems/notes/13. Multi biometric.md",
-    "Biometric Systems/notes/4. Face detection.md",
     "Senza nome.canvas"
   ]
 }

Concurrent Systems/notes/3.md

@@ -154,4 +154,13 @@ Without it, if two process $i$ and $j$ sets MY_TURN at the same time, then $i$ g
 
 *Proof:*
 - let t be the value of `MY_TURN[i]` after $p_{i}$ exits the doorway (after flag <- down)
-- when $p_j$ computes its ticket, it reads $t$ from `MY_TURN[i]`, it reads t from MY_TURNpi
+- when $p_j$ computes its ticket, it reads $t$ from `MY_TURN[i]`, it reads t from `MY_TURN[i]` (no write overlapping with this read)
+- Hence, `MY_TURN[j]` is at least $t+1$.
+
+**Lemma 2:** Let $p_i$ be in the CS and $p_j$ is in the doorway or in the bakery; then, $$⟨MY\_TURN[i] , i⟩ < ⟨MY\_TURN[j] , j⟩$$*Proof:*
+If $p_i$ is in the CS, it has terminated its first wait for $j$
+	let's consider the read of `FLAG[j]` done by $p_i$ that terminates such wait
+	
+W.r.t. the execution of $p_j$, it can be that
+- this read overlaps with `FLAG[j] <- up` by Lemma 1, `MY_TURN[i] < MY_TURN[j]` and ok
+- this read is contained within the computation of `MY_TURN[j]`, but it's not possible, since `MY_TURN` is computed with the