From 71668594b5b58a2560f65ea52f783051d1439cdb Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 09:04:12 +0100 Subject: [PATCH] vault backup: 2025-03-18 09:04:12 --- Concurrent Systems/notes/6 - Atomicity.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 0949c9c..c7c8b66 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/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$ \ No newline at end of file +- $\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 + + +