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

Concurrent Systems/notes/6 - Atomicity.md

@@ -13,4 +13,10 @@ 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.
-- $f$
+- $\forall X :\hat{S}|_{X} \in semantics(X)$
+- $\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
+
+
+