vault backup: 2025-03-18 09:09:12

Concurrent Systems/notes/6 - Atomicity.md

@@ -14,9 +14,12 @@ 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$
 - If $res[op] <_{H} inv[op']$, then $res[op] <_{S} inv[op']$
 	- can rearrange events only if they overlap
 
+Given an history $\hat{K}$, we can define a binary relation on events $⟶_{K}$ s.t. (op, op’) ∈ ⟶K if and only if res[op] <K inv[op’]. We write op ⟶K op’ for denoting (op, op’) ∈ ⟶K. Hence, condition 3 of the previous Def. requires that ⟶H ⊆ ⟶S.
 
+![[Pasted image 20250318090733.png]]
 
+![[Pasted image 20250318090909.png]]