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

Concurrent Systems/notes/6 - Atomicity.md

@@ -91,11 +91,16 @@ Posso quindi dire: $$<_{\hat{S}_X} \space = \space\to_X\space \subseteq\space \s
 
 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$
+Inoltre, dico che, For all process p, $\hat{H}|_p=inv(op1_p)res(op1_p)inv(op2_p)res(op2_p)...$, e questo è vero perché lo storico delle operazioni eseguite DA UN SOLO PROCESSO non può non essere sequenziale!
+
+E siccome
+- $op1_p \to_H op2_p \to_H \dots$ 
+- $\to_H \space \subseteq \space \to'$
+
+
+
+
+
 > [!PDF|red] class 6, p.6>  we would have a cycle of length 
 > 
 > we would contraddict op2 ->x op3
-
-...
-...
-