From efcd98f2d35caac5160ae2253d40ac52a26ec8dc Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 17:30:04 +0100 Subject: [PATCH] vault backup: 2025-03-18 17:30:04 --- .obsidian/workspace.json | 6 ++++-- Concurrent Systems/notes/6 - Atomicity.md | 7 ++++--- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index a8644e3..b44ffbb 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -6,6 +6,7 @@ { "id": "4c1f5b7a6abb1339", "type": "tabs", + "dimension": 50.63775510204081, "children": [ { "id": "51157f32453cba69", @@ -26,6 +27,7 @@ { "id": "4ae2dccd2d32173d", "type": "tabs", + "dimension": 49.36224489795919, "children": [ { "id": "88f2e3a5b973712d", @@ -36,8 +38,8 @@ "file": "Concurrent Systems/slides/class 6.pdf", "page": 6, "left": -23, - "top": 379, - "zoom": 0.6627078384798101 + "top": 584, + "zoom": 0.6538004750593824 }, "icon": "lucide-file-text", "title": "class 6" diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 7695939..24c0ed6 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -69,15 +69,16 @@ This said, we can say that **every DAG admits a topological order** (a total ord Let us define a linearization of $\hat{H}$ as follows: $$\hat{S}=inv(op1)res(op1)inv(op2)res(op2)...$$ we would have the topological order: $op1\to'op2\to'...$ -$\to'_X$ +$\to'|_X$ $\to|_X$ $\to_X$ -Si ha che $\to|_X \space \subseteq \space \to'_X$ perché l'ordinamento topologico è letteralmente la sequenza di eventi in $\hat{S}$ +Osservazione: $\to'|_X$ è come dire $\to_{\hat{S}|X}$, infatti l'ordinamento topologico +Si ha che $\to|_X \space \subseteq \space \to'|_X$ perché l'ordinamento topologico è letteralmente la sequenza di eventi in $\hat{S}$ $\hat{S}$ is clearly sequential. Moreover: 1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$, indeed: - - $<_{\hat{S}_X} \space = \space\to_X\space \subseteq\space \space\to|_X\space \subseteq\space \to'_X\space = \space\to_{\hat{S}|X}\space=\space<_{\hat{S}|X}$ + - $<_{\hat{S}_X} \space = \space\to_X\space \subseteq\space \space\to|_X\space \subseteq\space \to'|_X\space = \space\to_{\hat{S}|X}\space=\space<_{\hat{S}|X}$ - commento per non diventare scemi: - $\hat{S}_X$ lo storico ottenuto linearizzando $\hat{H}|_X$ - definisce una relazione di ordinamento $\to_X$