From 0a58fa122d25edcdd2775865e47debe149b7ff4a Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 18:00:04 +0100 Subject: [PATCH] vault backup: 2025-03-18 18:00:04 --- .obsidian/workspace.json | 6 +++--- Concurrent Systems/notes/6 - Atomicity.md | 4 +++- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 6c1d4f2..c13a352 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -4,12 +4,12 @@ "type": "split", "children": [ { - "id": "4c1f5b7a6abb1339", + "id": "f51c1efa0452f785", "type": "tabs", "dimension": 50.63775510204081, "children": [ { - "id": "51157f32453cba69", + "id": "681355c2483f6307", "type": "leaf", "state": { "type": "markdown", @@ -216,7 +216,7 @@ "companion:Toggle completion": false } }, - "active": "51157f32453cba69", + "active": "681355c2483f6307", "lastOpenFiles": [ "Concurrent Systems/slides/class 6.pdf", "Concurrent Systems/notes/6 - Atomicity.md", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index ee9512c..36bdd18 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -79,7 +79,9 @@ Considero $\to'|_X$ come $\to'$ filtrato per gli eventi su X. Considero $\to|_X$ come $\to$ filtrato per gli eventi di X. Da non confondere con $\to_X$ che invece è l'ordinamento su $\hat{S}_X$. Ricordiamoci che $\to$ è l'unione di $\to_X, \to_Y, \to_Z...$, E DI $\to_H$. -Si ha che $\to|_X \space \subseteq \space \to'|_X$ +Per come abbiamo appena definito $\to|_X$, è chiaro che sicuramente abbiamo che $\to_X \subseteq \to|_X$, in quanto $\to$ contiene chiaramente $\to_X$, ma $\to|_X$ può contenere anche elementi di $\to_H$. + +Si ha poi che $\to|_X \space \subseteq \space \to'|_X$ , perché $\to'$ è un ordinamento topologico di $\to$, quindi deve rispettare tutti i vincoli di precedenza imposti da $\to$. $\hat{S}$ is clearly sequential. Moreover: 1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$, indeed: