vault backup: 2025-03-18 15:24:57

Concurrent Systems/notes/6 - Atomicity.md

@@ -14,7 +14,7 @@ A history is **complete** if every inv is eventually followed by a corresponding
 ### Linearizability
 A complete history $\hat{H}$ is **linearizable** if there exists a sequential history $\hat{S}$ s.t.
 - $\forall X :\hat{S}|_{X} \in semantics(X)$
-- $\forall p:\hat{H}|_{p} = \hat{S}|p$
+- $\forall p:\hat{H}|_{p} = \hat{S}|_p$
 	- cannot swap actions performed by the same process
 - If $res[op] <_{H} inv[op']$, then $res[op] <_{S} inv[op']$
 	- can rearrange events only if they overlap
@@ -24,6 +24,7 @@ Given an history $\hat{K}$, we can define a binary relation on events $⟶_{K}$
 ![[Pasted image 20250318090733.png]]
 
 ![[Pasted image 20250318090909.png]]But there is another linearization possible! I can also push a before if I pull it before c!
+Of course I have to respect the semantics of a Queue (if I push "a" first, I have to pop "a" first because it's a fucking FIFO)
 
 #### Compositionality theorem
 $\hat{H}$ is linearizable if $\hat{H}|_{X}$ is linearizable, for all X in H
@@ -34,7 +35,10 @@ For all X, let $\hat{S}_{X}$ be a linearization of $\hat{H}_{X}$
 
 Let $\to$ denote $\to_{H} \cup \bigcup_{X \in H} \to _{X}$
 
-...
+We now show that $->$ is acyclic.
+
+
+
 > [!PDF|red] class 6, p.6>  we would have a cycle of length 
 > 
 > we would contraddict op2 ->x op3