vault backup: 2025-03-18 16:45:04

Concurrent Systems/notes/6 - Atomicity.md

@@ -66,9 +66,11 @@ We now show that $\to$ is acyclic.
 
 This said, we can say that **every DAG admits a topological order** (a total order of its nodes that respects the edges), we will call $\to'$ the topological order for $\to$
 
-Let us define a linearization of $\hat{H}$ as follows: $$\hat{S}=inv(op1)res(op1)$$
-
+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'...$
 
+$\hat{S}$ is clearly sequential. Moreover:
+1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$. Indeed:
 > [!PDF|red] class 6, p.6>  we would have a cycle of length 
 > 
 > we would contraddict op2 ->x op3