From 243dac16caa2788421d65a5d4ede2960fd5c8669 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 15:24:57 +0100 Subject: [PATCH] vault backup: 2025-03-18 15:24:57 --- .obsidian/workspace.json | 26 ++++++----------------- Concurrent Systems/notes/6 - Atomicity.md | 8 +++++-- 2 files changed, 13 insertions(+), 21 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 0bbdbcb..ec77d71 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -6,7 +6,7 @@ { "id": "4c1f5b7a6abb1339", "type": "tabs", - "dimension": 44.412607449856736, + "dimension": 44.41260744985673, "children": [ { "id": "51157f32453cba69", @@ -27,7 +27,7 @@ { "id": "e12a3c14771a10e5", "type": "tabs", - "dimension": 55.587392550143264, + "dimension": 55.58739255014327, "children": [ { "id": "f04931d588bd12d2", @@ -35,11 +35,7 @@ "state": { "type": "pdf", "state": { - "file": "Concurrent Systems/slides/class 6.pdf", - "page": 6, - "left": -23, - "top": 546, - "zoom": 0.6448931116389549 + "file": "Concurrent Systems/slides/class 6.pdf" }, "icon": "lucide-file-text", "title": "class 6" @@ -103,8 +99,7 @@ } ], "direction": "horizontal", - "width": 307.5, - "collapsed": true + "width": 307.5 }, "right": { "id": "bc4b945ded1926e3", @@ -178,8 +173,8 @@ "state": { "type": "git-view", "state": {}, - "icon": "git-pull-request", - "title": "Source Control" + "icon": "lucide-file", + "title": "Plugin no longer active" } }, { @@ -209,14 +204,7 @@ "canvas:Create new canvas": false, "daily-notes:Open today's daily note": false, "templates:Insert template": false, - "command-palette:Open command palette": false, - "obsidian-ocr:Search OCR": false, - "pdf-plus:PDF++: Toggle auto-copy": false, - "pdf-plus:PDF++: Toggle auto-focus": false, - "pdf-plus:PDF++: Toggle auto-paste": false, - "obsidian-git:Open Git source control": false, - "smart-second-brain:Open S2B Chat": false, - "companion:Toggle completion": false + "command-palette:Open command palette": false } }, "active": "51157f32453cba69", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 88a40ea..2677684 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/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