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

.obsidian/workspace.json

@@ -36,9 +36,9 @@
               "type": "pdf",
               "state": {
                 "file": "Concurrent Systems/slides/class 6.pdf",
-                "page": 6,
+                "page": 7,
                 "left": -23,
-                "top": 508,
+                "top": 496,
                 "zoom": 0.6538004750593824
               },
               "icon": "lucide-file-text",

Concurrent Systems/notes/6 - Atomicity.md

@@ -68,10 +68,7 @@ This said, we can say that **every DAG admits a topological order** (a total ord
 
 Let us define a linearization of $\hat{H}$ as follows: $$\hat{S}=inv(op1)res(op1)inv(op2)res(op2)...$$
 we would have the topological order: $op1\to'op2\to'...$
-
-$\to'|_X$
-$\to|_X$
-$\to_X$
+$\hat{S}$ is clearly sequential.
 
 Considero $\to'|_X$ come $\to'$ filtrato per gli eventi su X.
 
@@ -81,17 +78,20 @@ Considero $\to|_X$ come $\to$ filtrato per gli eventi di X. Da non confondere co
 
 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$.
+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$. Non sono necessariamente uguali perché l'ordinamento topologico può imporre ulteriori ordinamenti tra eventi che in $ non erano esplicitamente vincolati.
 
-$\hat{S}$ is clearly sequential. Moreover:
-1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$, indeed:
-	- $<_{\hat{S}_X} \space = \space\to_X\space \subseteq\space \space\to|_X\space \subseteq\space \to'|_X\space = \space\to_{\hat{S}|X}\space=\space<_{\hat{S}|X}$
-		- commento per non diventare scemi:
+
+Posso quindi dire: $$<_{\hat{S}_X} \space = \space\to_X\space \subseteq\space \space\to|_X\space \subseteq\space \to'|_X\space = \space\to_{\hat{S}|X}\space=\space<_{\hat{S}|X}$$		ricordando:
 			- $\hat{S}_X$ lo storico ottenuto linearizzando $\hat{H}|_X$ 
 				- definisce una relazione di ordinamento $\to_X$ 
 			- $\hat{S}|_X$ lo storico che ottengo filtrando per le operazioni su X, partendo da $\hat{S}$, che a sua volta viene ottenuto linearizzando $\hat{H}$
 				- definisce una relazione di ordinamento $\to|_{\hat{S}_X}$ 
 			- naturlamente, possiamo considerare $\to_X \space = \space <_{\hat{S}_X}$ e $\to|_{\hat{S}_X} \space = \space <_{\hat{S}|_X}$ (se l'ordinamento è uguale, allora anche le coppie in relazione tra loro sono le stesse)
+
+
+E allora si ha come corollario che$$\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$$
+
+Inoltre, dico che, For all p, $\hat{H}|_p=inv(op1_p)res(op1_p)inv(op2_p)res(op2_p$
 > [!PDF|red] class 6, p.6>  we would have a cycle of length 
 > 
 > we would contraddict op2 ->x op3