vault backup: 2025-03-18 18:00:04

.obsidian/workspace.json

@@ -4,12 +4,12 @@
     "type": "split",
     "children": [
       {
-        "id": "4c1f5b7a6abb1339",
+        "id": "f51c1efa0452f785",
         "type": "tabs",
         "dimension": 50.63775510204081,
         "children": [
           {
-            "id": "51157f32453cba69",
+            "id": "681355c2483f6307",
             "type": "leaf",
             "state": {
               "type": "markdown",
@@ -216,7 +216,7 @@
       "companion:Toggle completion": false
     }
   },
-  "active": "51157f32453cba69",
+  "active": "681355c2483f6307",
   "lastOpenFiles": [
     "Concurrent Systems/slides/class 6.pdf",
     "Concurrent Systems/notes/6 - Atomicity.md",

Concurrent Systems/notes/6 - Atomicity.md

@@ -79,7 +79,9 @@ Considero $\to'|_X$ come $\to'$ filtrato per gli eventi su X.
 
 Considero $\to|_X$ come $\to$ filtrato per gli eventi di X. Da non confondere con $\to_X$ che invece è l'ordinamento su $\hat{S}_X$. Ricordiamoci che $\to$ è l'unione di $\to_X, \to_Y, \to_Z...$, E DI $\to_H$.
 
-Si ha che $\to|_X \space \subseteq \space \to'|_X$ 
+Per come abbiamo appena definito $\to|_X$, è chiaro che sicuramente abbiamo che $\to_X \subseteq \to|_X$, in quanto $\to$ contiene chiaramente $\to_X$, ma $\to|_X$ può contenere anche elementi di $\to_H$.
+
+Si ha poi che $\to|_X \space \subseteq \space \to'|_X$ , perché $\to'$ è un ordinamento topologico di $\to$, quindi deve rispettare tutti i vincoli di precedenza imposti da $\to$.
 
 $\hat{S}$ is clearly sequential. Moreover:
 1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$, indeed: