From 243dac16caa2788421d65a5d4ede2960fd5c8669 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 15:24:57 +0100 Subject: [PATCH 01/39] 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 From d3b9c563dc2045617f0da09edb9abc41363906bf Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 15:30:04 +0100 Subject: [PATCH 02/39] vault backup: 2025-03-18 15:30:04 --- .obsidian/community-plugins.json | 1 - .obsidian/workspace.json | 34 +++++++++++------- Concurrent Systems/notes/6 - Atomicity.md | 6 +++- .../images/Pasted image 20250318090733.png | Bin .../images/Pasted image 20250318090909.png | Bin 5 files changed, 26 insertions(+), 15 deletions(-) rename Pasted image 20250318090733.png => Concurrent Systems/notes/images/Pasted image 20250318090733.png (100%) rename Pasted image 20250318090909.png => Concurrent Systems/notes/images/Pasted image 20250318090909.png (100%) diff --git a/.obsidian/community-plugins.json b/.obsidian/community-plugins.json index 49ffe43..0871a1f 100644 --- a/.obsidian/community-plugins.json +++ b/.obsidian/community-plugins.json @@ -5,6 +5,5 @@ "mathlive-in-editor-mode", "smart-second-brain", "local-gpt", - "obsidian-latex-suite", "companion" ] \ No newline at end of file diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index ec77d71..2ab0866 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -6,7 +6,6 @@ { "id": "4c1f5b7a6abb1339", "type": "tabs", - "dimension": 44.41260744985673, "children": [ { "id": "51157f32453cba69", @@ -25,17 +24,20 @@ ] }, { - "id": "e12a3c14771a10e5", + "id": "4ae2dccd2d32173d", "type": "tabs", - "dimension": 55.58739255014327, "children": [ { - "id": "f04931d588bd12d2", + "id": "88f2e3a5b973712d", "type": "leaf", "state": { "type": "pdf", "state": { - "file": "Concurrent Systems/slides/class 6.pdf" + "file": "Concurrent Systems/slides/class 6.pdf", + "page": 5, + "left": -19, + "top": 573, + "zoom": 0.7998812351543944 }, "icon": "lucide-file-text", "title": "class 6" @@ -94,12 +96,12 @@ "title": "Segnalibri" } } - ], - "currentTab": 1 + ] } ], "direction": "horizontal", - "width": 307.5 + "width": 307.5, + "collapsed": true }, "right": { "id": "bc4b945ded1926e3", @@ -204,15 +206,21 @@ "canvas:Create new canvas": false, "daily-notes:Open today's daily note": false, "templates:Insert template": false, - "command-palette:Open command palette": 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, + "companion:Toggle completion": false } }, - "active": "51157f32453cba69", + "active": "88f2e3a5b973712d", "lastOpenFiles": [ - "Concurrent Systems/slides/class 6.pdf", "Concurrent Systems/notes/6 - Atomicity.md", - "Pasted image 20250318090909.png", - "Pasted image 20250318090733.png", + "Concurrent Systems/slides/class 6.pdf", + "Concurrent Systems/notes/images/Pasted image 20250318090733.png", + "Concurrent Systems/notes/images/Pasted image 20250318090909.png", "Concurrent Systems/slides/class 5.pdf", "Concurrent Systems/notes/5 - Software Transactional Memory.md", "Concurrent Systems/notes/4c - Dining Philosophers.md", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 2677684..3890270 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -35,8 +35,12 @@ 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. +We now show that $\to$ is acyclic. +1. It cannot have cycles with 1 edge (i.e. self loops): indeed, if $op \to op$, this would mean that $res(op) < inv(op)$, which of course does not make any sense. +2. it cannot have cycles with 2 edges: + - let's assume that $op \to op' \to op$ + - both arrows cannot be $\to_H$ nor $\to_X$ (for some X) > [!PDF|red] class 6, p.6> we would have a cycle of length diff --git a/Pasted image 20250318090733.png b/Concurrent Systems/notes/images/Pasted image 20250318090733.png similarity index 100% rename from Pasted image 20250318090733.png rename to Concurrent Systems/notes/images/Pasted image 20250318090733.png diff --git a/Pasted image 20250318090909.png b/Concurrent Systems/notes/images/Pasted image 20250318090909.png similarity index 100% rename from Pasted image 20250318090909.png rename to Concurrent Systems/notes/images/Pasted image 20250318090909.png From 8f5c1274280297b39e03142120ebe1dc01644d87 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 15:35:04 +0100 Subject: [PATCH 03/39] vault backup: 2025-03-18 15:35:04 --- .obsidian/workspace.json | 6 +++--- Concurrent Systems/notes/6 - Atomicity.md | 3 ++- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 2ab0866..cc2b768 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -36,7 +36,7 @@ "file": "Concurrent Systems/slides/class 6.pdf", "page": 5, "left": -19, - "top": 573, + "top": 529, "zoom": 0.7998812351543944 }, "icon": "lucide-file-text", @@ -215,10 +215,10 @@ "companion:Toggle completion": false } }, - "active": "88f2e3a5b973712d", + "active": "51157f32453cba69", "lastOpenFiles": [ - "Concurrent Systems/notes/6 - Atomicity.md", "Concurrent Systems/slides/class 6.pdf", + "Concurrent Systems/notes/6 - Atomicity.md", "Concurrent Systems/notes/images/Pasted image 20250318090733.png", "Concurrent Systems/notes/images/Pasted image 20250318090909.png", "Concurrent Systems/slides/class 5.pdf", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 3890270..a39c7f5 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -40,7 +40,8 @@ We now show that $\to$ is acyclic. 2. it cannot have cycles with 2 edges: - let's assume that $op \to op' \to op$ - - both arrows cannot be $\to_H$ nor $\to_X$ (for some X) + - both arrows cannot be $\to_H$ nor $\to_X$ (for some X), otw. it won't be a total order (and would be cyclic) + - it cannot be that one is $\to_X$ > [!PDF|red] class 6, p.6> we would have a cycle of length From 3e3e4cffc62f554d51ac13d55d6b873a53421645 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 15:40:04 +0100 Subject: [PATCH 04/39] vault backup: 2025-03-18 15:40:04 --- Concurrent Systems/notes/6 - Atomicity.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index a39c7f5..26841e7 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -41,7 +41,8 @@ We now show that $\to$ is acyclic. 2. it cannot have cycles with 2 edges: - let's assume that $op \to op' \to op$ - both arrows cannot be $\to_H$ nor $\to_X$ (for some X), otw. it won't be a total order (and would be cyclic) - - it cannot be that one is $\to_X$ + - it cannot be that one is $\to_X$ and the other $\to_Y$ (for some $X \neq Y$), otherwise op/op' would be on 2 different objects. + - So it must be $op \to_X op' \to_H op$ > [!PDF|red] class 6, p.6> we would have a cycle of length From 4bc441c75d78546b518ab888565243a25f02fa66 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 15:45:04 +0100 Subject: [PATCH 05/39] vault backup: 2025-03-18 15:45:04 --- Concurrent Systems/notes/6 - Atomicity.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 26841e7..86f3ea4 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -42,7 +42,8 @@ We now show that $\to$ is acyclic. - let's assume that $op \to op' \to op$ - both arrows cannot be $\to_H$ nor $\to_X$ (for some X), otw. it won't be a total order (and would be cyclic) - it cannot be that one is $\to_X$ and the other $\to_Y$ (for some $X \neq Y$), otherwise op/op' would be on 2 different objects. - - So it must be $op \to_X op' \to_H op$ + - **So it must b**e $op \to_X op' \to_H op$ (or vice versa) + - then, $op' \to op$ means that $r$ > [!PDF|red] class 6, p.6> we would have a cycle of length From 36a06a3c35d60a0b65ba87aa076f5a770568d1c8 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 15:50:04 +0100 Subject: [PATCH 06/39] vault backup: 2025-03-18 15:50:04 --- Concurrent Systems/notes/6 - Atomicity.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 86f3ea4..d54f470 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -32,6 +32,7 @@ $\hat{H}$ is linearizable if $\hat{H}|_{X}$ is linearizable, for all X in H For all X, let $\hat{S}_{X}$ be a linearization of $\hat{H}_{X}$ - $\hat{S}_{X}$ defines a total order on the operations on X (call it $\to_{X}$) + - a union of relations is a union of pairs! Let $\to$ denote $\to_{H} \cup \bigcup_{X \in H} \to _{X}$ @@ -43,7 +44,8 @@ We now show that $\to$ is acyclic. - both arrows cannot be $\to_H$ nor $\to_X$ (for some X), otw. it won't be a total order (and would be cyclic) - it cannot be that one is $\to_X$ and the other $\to_Y$ (for some $X \neq Y$), otherwise op/op' would be on 2 different objects. - **So it must b**e $op \to_X op' \to_H op$ (or vice versa) - - then, $op' \to op$ means that $r$ + - then, $op' \to op$ means that $res(op') <_H inv(op)$ + - Since $\hat{S}_X$ is a linearization of $\hat{H}|_X$ and op/op' are on X, this implies $res(op') <_X inv(op)$, which means that $op' \to_X op$, and so $\to_X$ would be cyclic. > [!PDF|red] class 6, p.6> we would have a cycle of length From fc4341f99c723661f2fc418cbbb7d0251d3df46a Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 15:55:04 +0100 Subject: [PATCH 07/39] vault backup: 2025-03-18 15:55:04 --- .obsidian/workspace.json | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index cc2b768..7197b2b 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -36,7 +36,7 @@ "file": "Concurrent Systems/slides/class 6.pdf", "page": 5, "left": -19, - "top": 529, + "top": 437, "zoom": 0.7998812351543944 }, "icon": "lucide-file-text", @@ -215,10 +215,10 @@ "companion:Toggle completion": false } }, - "active": "51157f32453cba69", + "active": "88f2e3a5b973712d", "lastOpenFiles": [ - "Concurrent Systems/slides/class 6.pdf", "Concurrent Systems/notes/6 - Atomicity.md", + "Concurrent Systems/slides/class 6.pdf", "Concurrent Systems/notes/images/Pasted image 20250318090733.png", "Concurrent Systems/notes/images/Pasted image 20250318090909.png", "Concurrent Systems/slides/class 5.pdf", From 4d9cc3b2e192b3d990fafe0094391a542a11daf7 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 16:00:04 +0100 Subject: [PATCH 08/39] vault backup: 2025-03-18 16:00:04 --- .obsidian/community-plugins.json | 4 ++-- .obsidian/workspace.json | 15 +++++++-------- Concurrent Systems/notes/6 - Atomicity.md | 9 ++++++--- 3 files changed, 15 insertions(+), 13 deletions(-) diff --git a/.obsidian/community-plugins.json b/.obsidian/community-plugins.json index 0871a1f..dc1b1be 100644 --- a/.obsidian/community-plugins.json +++ b/.obsidian/community-plugins.json @@ -1,9 +1,9 @@ [ "obsidian-ocr", - "pdf-plus", "obsidian-git", "mathlive-in-editor-mode", "smart-second-brain", "local-gpt", - "companion" + "companion", + "pdf-plus" ] \ No newline at end of file diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 7197b2b..d2db11a 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -34,10 +34,10 @@ "type": "pdf", "state": { "file": "Concurrent Systems/slides/class 6.pdf", - "page": 5, - "left": -19, - "top": 437, - "zoom": 0.7998812351543944 + "page": 4, + "left": -23, + "top": 143, + "zoom": 0.6627078384798101 }, "icon": "lucide-file-text", "title": "class 6" @@ -100,8 +100,7 @@ } ], "direction": "horizontal", - "width": 307.5, - "collapsed": true + "width": 307.5 }, "right": { "id": "bc4b945ded1926e3", @@ -215,10 +214,10 @@ "companion:Toggle completion": false } }, - "active": "88f2e3a5b973712d", + "active": "51157f32453cba69", "lastOpenFiles": [ - "Concurrent Systems/notes/6 - Atomicity.md", "Concurrent Systems/slides/class 6.pdf", + "Concurrent Systems/notes/6 - Atomicity.md", "Concurrent Systems/notes/images/Pasted image 20250318090733.png", "Concurrent Systems/notes/images/Pasted image 20250318090909.png", "Concurrent Systems/slides/class 5.pdf", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index d54f470..a2a7530 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -39,13 +39,16 @@ Let $\to$ denote $\to_{H} \cup \bigcup_{X \in H} \to _{X}$ We now show that $\to$ is acyclic. 1. It cannot have cycles with 1 edge (i.e. self loops): indeed, if $op \to op$, this would mean that $res(op) < inv(op)$, which of course does not make any sense. -2. it cannot have cycles with 2 edges: +2. It cannot have cycles with 2 edges: - let's assume that $op \to op' \to op$ - both arrows cannot be $\to_H$ nor $\to_X$ (for some X), otw. it won't be a total order (and would be cyclic) - it cannot be that one is $\to_X$ and the other $\to_Y$ (for some $X \neq Y$), otherwise op/op' would be on 2 different objects. - - **So it must b**e $op \to_X op' \to_H op$ (or vice versa) + - **So it must b**e $op \to_X op' \to_H op$ *(or vice versa)* - then, $op' \to op$ means that $res(op') <_H inv(op)$ - - Since $\hat{S}_X$ is a linearization of $\hat{H}|_X$ and op/op' are on X, this implies $res(op') <_X inv(op)$, which means that $op' \to_X op$, and so $\to_X$ would be cyclic. + - Since $\hat{S}_X$ is a linearization of $\hat{H}|_X$ and op/op' are on X (literally because we have op ->x op'), this implies $res(op') <_X inv(op)$, which means that $op' \to_X op$, and so it won't be a total order... So this is not possible either. + +3. It cannot have cycles with more than 2 edges: + 1. > [!PDF|red] class 6, p.6> we would have a cycle of length From 21069a115c6a50ae6c7090296a918a91d2cbb1b0 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 16:05:04 +0100 Subject: [PATCH 09/39] vault backup: 2025-03-18 16:05:04 --- .obsidian/workspace.json | 4 ++-- Concurrent Systems/notes/6 - Atomicity.md | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index d2db11a..c1c26a8 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -34,9 +34,9 @@ "type": "pdf", "state": { "file": "Concurrent Systems/slides/class 6.pdf", - "page": 4, + "page": 5, "left": -23, - "top": 143, + "top": 415, "zoom": 0.6627078384798101 }, "icon": "lucide-file-text", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index a2a7530..5616818 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -48,7 +48,8 @@ We now show that $\to$ is acyclic. - Since $\hat{S}_X$ is a linearization of $\hat{H}|_X$ and op/op' are on X (literally because we have op ->x op'), this implies $res(op') <_X inv(op)$, which means that $op' \to_X op$, and so it won't be a total order... So this is not possible either. 3. It cannot have cycles with more than 2 edges: - 1. + - by contradiction, consider a shortest cycle + - adjacent edges cannot belong to the same order (otw. the cycle would be shortable, because of transitivity) > [!PDF|red] class 6, p.6> we would have a cycle of length From 1e853b88f7f8bd43a449463e365d3530c0891b0f Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 16:10:04 +0100 Subject: [PATCH 10/39] vault backup: 2025-03-18 16:10:04 --- Concurrent Systems/notes/6 - Atomicity.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 5616818..d4f1ed9 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -49,7 +49,7 @@ We now show that $\to$ is acyclic. 3. It cannot have cycles with more than 2 edges: - by contradiction, consider a shortest cycle - - adjacent edges cannot belong to the same order (otw. the cycle would be shortable, because of transitivity) + - adjacent edges cannot belong to the same order (not both $\to_X$ ), otw. the cycle would be shortable, because of transitivity of the total order! > [!PDF|red] class 6, p.6> we would have a cycle of length From 9322e5e2735e208a79b3e5202b6ed91af80aac9a Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 16:15:04 +0100 Subject: [PATCH 11/39] vault backup: 2025-03-18 16:15:04 --- Concurrent Systems/notes/6 - Atomicity.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index d4f1ed9..c916083 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -49,7 +49,9 @@ We now show that $\to$ is acyclic. 3. It cannot have cycles with more than 2 edges: - by contradiction, consider a shortest cycle - - adjacent edges cannot belong to the same order (not both $\to_X$ ), otw. the cycle would be shortable, because of transitivity of the total order! + - adjacent edges cannot belong to the same order (e.g. not both $\to_X$), otw. the cycle would be shortable, because of transitivity of the total order! + - adjacent edges cannot belong to orders on different objects + - this would mean that an operation is involved in both $\to_X$ and $\to_Y$ > [!PDF|red] class 6, p.6> we would have a cycle of length From e9ad07bfd4186991dcea31851964bf3a76c797a5 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 16:20:04 +0100 Subject: [PATCH 12/39] vault backup: 2025-03-18 16:20:04 --- .obsidian/workspace.json | 2 +- Concurrent Systems/notes/6 - Atomicity.md | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index c1c26a8..2bcc1c5 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -36,7 +36,7 @@ "file": "Concurrent Systems/slides/class 6.pdf", "page": 5, "left": -23, - "top": 415, + "top": 360, "zoom": 0.6627078384798101 }, "icon": "lucide-file-text", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index c916083..9a7d052 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -51,7 +51,9 @@ We now show that $\to$ is acyclic. - by contradiction, consider a shortest cycle - adjacent edges cannot belong to the same order (e.g. not both $\to_X$), otw. the cycle would be shortable, because of transitivity of the total order! - adjacent edges cannot belong to orders on different objects - - this would mean that an operation is involved in both $\to_X$ and $\to_Y$ + - this would mean that an operation is involved in both $\to_X$ and $\to_Y$ but it is not possible of course + - Hence, at least one $\to_X$ exists and it must be between two $\to_H$ i.e.: $$op1 \to_H op2 \to_X op3 \to_H op4$$ + - can this be a cycle? > [!PDF|red] class 6, p.6> we would have a cycle of length From b1afe923d0e1cb12598062099194b6bb66b0fb7e Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 16:25:04 +0100 Subject: [PATCH 13/39] vault backup: 2025-03-18 16:25:04 --- Concurrent Systems/notes/6 - Atomicity.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 9a7d052..1552a13 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -52,8 +52,12 @@ We now show that $\to$ is acyclic. - adjacent edges cannot belong to the same order (e.g. not both $\to_X$), otw. the cycle would be shortable, because of transitivity of the total order! - adjacent edges cannot belong to orders on different objects - this would mean that an operation is involved in both $\to_X$ and $\to_Y$ but it is not possible of course - - Hence, at least one $\to_X$ exists and it must be between two $\to_H$ i.e.: $$op1 \to_H op2 \to_X op3 \to_H op4$$ + - Hence, at least one $\to_X$ exists and it must be between two $\to_H$ i.e.: $$op1 \to_H op2 \to_X op3 \to_H op4$$, with op1 = op4 - can this be a cycle? + - $op1 \to_H op2$ means that $res(op1) <_H inv(op2)$ + - $op2 \to_X op3$ entails that $inv(op2) <_H res(op3)$ + - if not, as is a total order, we would have that $res(op3) <_H inv(op2)$, but we then would have a cycle of lenght 2... + - $op2 \to_H op3$ entails that $inv(op2) <_H res(op3)$ > [!PDF|red] class 6, p.6> we would have a cycle of length From f09563169ce9f2856df692f454f5cc04ada29ed5 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 16:30:04 +0100 Subject: [PATCH 14/39] vault backup: 2025-03-18 16:30:04 --- .obsidian/workspace.json | 4 ++-- Concurrent Systems/notes/6 - Atomicity.md | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 2bcc1c5..cb59014 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -34,9 +34,9 @@ "type": "pdf", "state": { "file": "Concurrent Systems/slides/class 6.pdf", - "page": 5, + "page": 6, "left": -23, - "top": 360, + "top": 428, "zoom": 0.6627078384798101 }, "icon": "lucide-file-text", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 1552a13..0057b81 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -51,12 +51,12 @@ We now show that $\to$ is acyclic. - by contradiction, consider a shortest cycle - adjacent edges cannot belong to the same order (e.g. not both $\to_X$), otw. the cycle would be shortable, because of transitivity of the total order! - adjacent edges cannot belong to orders on different objects - - this would mean that an operation is involved in both $\to_X$ and $\to_Y$ but it is not possible of course - - Hence, at least one $\to_X$ exists and it must be between two $\to_H$ i.e.: $$op1 \to_H op2 \to_X op3 \to_H op4$$, with op1 = op4 + - this would mean that an operation is involved in both $\to_X$ and $\to_Y$ but it is not possible of course, so the cycle can only happen edges in $\to_X$ and $\to_H$. + - Hence, at least one $\to_X$ exists and it must be between two $\to_H$ i.e.: $$op1 \to_H op2 \to_X op3 \to_H op4$$, likely with op1 = op4 - can this be a cycle? - $op1 \to_H op2$ means that $res(op1) <_H inv(op2)$ - $op2 \to_X op3$ entails that $inv(op2) <_H res(op3)$ - - if not, as is a total order, we would have that $res(op3) <_H inv(op2)$, but we then would have a cycle of lenght 2... + - if not, as is a total order, we would have that $res(op3) <_H inv(op2)$, but we then would have $op3 \to_H op2$ a cycle of lenght 2... - $op2 \to_H op3$ entails that $inv(op2) <_H res(op3)$ From 32053062f6a0311811d09f6dbc767206af88db8d Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 16:35:04 +0100 Subject: [PATCH 15/39] vault backup: 2025-03-18 16:35:04 --- Concurrent Systems/notes/6 - Atomicity.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 0057b81..0827fae 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -56,8 +56,11 @@ We now show that $\to$ is acyclic. - can this be a cycle? - $op1 \to_H op2$ means that $res(op1) <_H inv(op2)$ - $op2 \to_X op3$ entails that $inv(op2) <_H res(op3)$ - - if not, as is a total order, we would have that $res(op3) <_H inv(op2)$, but we then would have $op3 \to_H op2$ a cycle of lenght 2... - - $op2 \to_H op3$ entails that $inv(op2) <_H res(op3)$ + - if not, as is a total order, we would have that $res(op3) <_H inv(op2)$, but we then would have $op3 \to_H op2$, forming a cycle of lenght 2 because $op2 \to_X op3$, and we know cycles of lenght 2 are not possible... + - $op3 \to_H op4$ means that $res(op3) <_H inv(op4)$ + + - We would then have that $res(op1) <_H inv(op2) <_H res(op3) <_H inv(op4)$ + - So by transitivity $res(op1) <_H inv(op4)$ > [!PDF|red] class 6, p.6> we would have a cycle of length From 7092fd7c4d8c4c956e8dc3ecdf09fd9e02eb0f01 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 16:40:04 +0100 Subject: [PATCH 16/39] vault backup: 2025-03-18 16:40:04 --- 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 0827fae..687889b 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -60,7 +60,13 @@ We now show that $\to$ is acyclic. - $op3 \to_H op4$ means that $res(op3) <_H inv(op4)$ - We would then have that $res(op1) <_H inv(op2) <_H res(op3) <_H inv(op4)$ - - So by transitivity $res(op1) <_H inv(op4)$ + - So by transitivity $res(op1) <_H inv(op4)$, i.e. $op1 \to_H op4$ + - IN CONTRADICTION WITH HAVING CHOSEN A SHORTEST CYCLE + - as if op4 = op1, then this could not happen as $\to$ is a total order. + +This said, we can say that **every DAG admits a topological order** (a total order of its nodes that respects the edges), we will call $\to'$ the topological order for $\to$ + +Let us define a linearization of $\hat{H}$ as follows: $$\hat{S}=inv(op1)res(op1)$$ > [!PDF|red] class 6, p.6> we would have a cycle of length From 2b88b8deb03971151a349d49e0f07ab508085908 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 16:45:04 +0100 Subject: [PATCH 17/39] vault backup: 2025-03-18 16:45:04 --- Concurrent Systems/notes/6 - Atomicity.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 687889b..fe345c0 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -66,9 +66,11 @@ We now show that $\to$ is acyclic. This said, we can say that **every DAG admits a topological order** (a total order of its nodes that respects the edges), we will call $\to'$ the topological order for $\to$ -Let us define a linearization of $\hat{H}$ as follows: $$\hat{S}=inv(op1)res(op1)$$ - +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'...$ +$\hat{S}$ is clearly sequential. Moreover: +1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$. Indeed: > [!PDF|red] class 6, p.6> we would have a cycle of length > > we would contraddict op2 ->x op3 From b10d2828fa1aed2910f4f5ac6f4a3547bf01dbfa Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 16:50:04 +0100 Subject: [PATCH 18/39] vault backup: 2025-03-18 16:50:04 --- .obsidian/workspace.json | 2 +- Concurrent Systems/notes/6 - Atomicity.md | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index cb59014..42e4b3d 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -36,7 +36,7 @@ "file": "Concurrent Systems/slides/class 6.pdf", "page": 6, "left": -23, - "top": 428, + "top": 259, "zoom": 0.6627078384798101 }, "icon": "lucide-file-text", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index fe345c0..3f44007 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -71,6 +71,8 @@ we would have the topological order: $op1\to'op2\to'...$ $\hat{S}$ is clearly sequential. Moreover: 1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$. Indeed: + - $<_{\hat{S}_X}=\to_X \subseteq \to'_X = \to_{\hat{S}|X}=<_{\hat{S}|X}$ + - > [!PDF|red] class 6, p.6> we would have a cycle of length > > we would contraddict op2 ->x op3 From 2f2a31c93bdc79f0cfde7f5b384d7c6f993264cf Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 16:55:04 +0100 Subject: [PATCH 19/39] vault backup: 2025-03-18 16:55:04 --- .obsidian/workspace.json | 6 +++--- Concurrent Systems/notes/6 - Atomicity.md | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 42e4b3d..2874e26 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -36,7 +36,7 @@ "file": "Concurrent Systems/slides/class 6.pdf", "page": 6, "left": -23, - "top": 259, + "top": 242, "zoom": 0.6627078384798101 }, "icon": "lucide-file-text", @@ -214,10 +214,10 @@ "companion:Toggle completion": false } }, - "active": "51157f32453cba69", + "active": "88f2e3a5b973712d", "lastOpenFiles": [ - "Concurrent Systems/slides/class 6.pdf", "Concurrent Systems/notes/6 - Atomicity.md", + "Concurrent Systems/slides/class 6.pdf", "Concurrent Systems/notes/images/Pasted image 20250318090733.png", "Concurrent Systems/notes/images/Pasted image 20250318090909.png", "Concurrent Systems/slides/class 5.pdf", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 3f44007..1954aa7 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -70,7 +70,7 @@ Let us define a linearization of $\hat{H}$ as follows: $$\hat{S}=inv(op1)res(op1 we would have the topological order: $op1\to'op2\to'...$ $\hat{S}$ is clearly sequential. Moreover: -1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$. Indeed: +1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$, indeed: - $<_{\hat{S}_X}=\to_X \subseteq \to'_X = \to_{\hat{S}|X}=<_{\hat{S}|X}$ - > [!PDF|red] class 6, p.6> we would have a cycle of length From 11990402bc7b2902de6c42a20c1c7f35373f2a15 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 17:00:04 +0100 Subject: [PATCH 20/39] vault backup: 2025-03-18 17:00:04 --- .obsidian/workspace.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 2874e26..d236356 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -36,7 +36,7 @@ "file": "Concurrent Systems/slides/class 6.pdf", "page": 6, "left": -23, - "top": 242, + "top": 283, "zoom": 0.6627078384798101 }, "icon": "lucide-file-text", From d5474248df5be0b451ab0d7d110665c6429dc9ae Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 17:05:04 +0100 Subject: [PATCH 21/39] vault backup: 2025-03-18 17:05:04 --- .obsidian/workspace.json | 6 +++--- Concurrent Systems/notes/6 - Atomicity.md | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index d236356..a8644e3 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -36,7 +36,7 @@ "file": "Concurrent Systems/slides/class 6.pdf", "page": 6, "left": -23, - "top": 283, + "top": 379, "zoom": 0.6627078384798101 }, "icon": "lucide-file-text", @@ -214,10 +214,10 @@ "companion:Toggle completion": false } }, - "active": "88f2e3a5b973712d", + "active": "51157f32453cba69", "lastOpenFiles": [ - "Concurrent Systems/notes/6 - Atomicity.md", "Concurrent Systems/slides/class 6.pdf", + "Concurrent Systems/notes/6 - Atomicity.md", "Concurrent Systems/notes/images/Pasted image 20250318090733.png", "Concurrent Systems/notes/images/Pasted image 20250318090909.png", "Concurrent Systems/slides/class 5.pdf", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 1954aa7..77c3499 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -72,7 +72,7 @@ we would have the topological order: $op1\to'op2\to'...$ $\hat{S}$ is clearly sequential. Moreover: 1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$, indeed: - $<_{\hat{S}_X}=\to_X \subseteq \to'_X = \to_{\hat{S}|X}=<_{\hat{S}|X}$ - - + - commenti > [!PDF|red] class 6, p.6> we would have a cycle of length > > we would contraddict op2 ->x op3 From ee993e660ea3144b8645ccb230f2ba03e1c8ecd0 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 17:10:04 +0100 Subject: [PATCH 22/39] vault backup: 2025-03-18 17:10:04 --- Concurrent Systems/notes/6 - Atomicity.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 77c3499..1a11de8 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -72,7 +72,11 @@ we would have the topological order: $op1\to'op2\to'...$ $\hat{S}$ is clearly sequential. Moreover: 1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$, indeed: - $<_{\hat{S}_X}=\to_X \subseteq \to'_X = \to_{\hat{S}|X}=<_{\hat{S}|X}$ - - commenti + - commento per non diventare scemi: + - $\hat{S}_X$ lo storico ottenuto linearizzando $\hat{H}|_X$ + - $\hat{S}|_X$ lo storico che ottengo filtrando per le operazioni su X, partendo da $\hat{S}$, che a sua volta viene ottenuto linearizzando $\hat{H}$ + - $\to_X$ + - $\to|_X$ > [!PDF|red] class 6, p.6> we would have a cycle of length > > we would contraddict op2 ->x op3 From e6d2ed4aed2347b87589914f33228f9d470f3e9c Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 17:15:04 +0100 Subject: [PATCH 23/39] vault backup: 2025-03-18 17:15:04 --- Concurrent Systems/notes/6 - Atomicity.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 1a11de8..64f5111 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -74,9 +74,9 @@ $\hat{S}$ is clearly sequential. Moreover: - $<_{\hat{S}_X}=\to_X \subseteq \to'_X = \to_{\hat{S}|X}=<_{\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$ - $\hat{S}|_X$ lo storico che ottengo filtrando per le operazioni su X, partendo da $\hat{S}$, che a sua volta viene ottenuto linearizzando $\hat{H}$ - - $\to_X$ - - $\to|_X$ + - definisce una relazione di ordinamento $\to|_X$ > [!PDF|red] class 6, p.6> we would have a cycle of length > > we would contraddict op2 ->x op3 From bf1a229fa523af79c05f470bc0d606aa48747d74 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 17:20:04 +0100 Subject: [PATCH 24/39] vault backup: 2025-03-18 17:20:04 --- .obsidian/workspace.json | 4 ++-- Concurrent Systems/notes/6 - Atomicity.md | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index a8644e3..b306be6 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -214,10 +214,10 @@ "companion:Toggle completion": false } }, - "active": "51157f32453cba69", + "active": "88f2e3a5b973712d", "lastOpenFiles": [ - "Concurrent Systems/slides/class 6.pdf", "Concurrent Systems/notes/6 - Atomicity.md", + "Concurrent Systems/slides/class 6.pdf", "Concurrent Systems/notes/images/Pasted image 20250318090733.png", "Concurrent Systems/notes/images/Pasted image 20250318090909.png", "Concurrent Systems/slides/class 5.pdf", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 64f5111..b34c210 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -71,12 +71,13 @@ we would have the topological order: $op1\to'op2\to'...$ $\hat{S}$ is clearly sequential. Moreover: 1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$, indeed: - - $<_{\hat{S}_X}=\to_X \subseteq \to'_X = \to_{\hat{S}|X}=<_{\hat{S}|X}$ + - $<_{\hat{S}_X} \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$ - $\hat{S}|_X$ lo storico che ottengo filtrando per le operazioni su X, partendo da $\hat{S}$, che a sua volta viene ottenuto linearizzando $\hat{H}$ - definisce una relazione di ordinamento $\to|_X$ + - naturlamente, possiamo considerare $\to_X \space = \space <_{\hat{S}_X}$ e $\to|_X \space = \space <_{\hat{S}|_X}$ (se l'ordinamento è uguale, allora anche le coppie in relazione tra loro sono le stesse) > [!PDF|red] class 6, p.6> we would have a cycle of length > > we would contraddict op2 ->x op3 From 9afe2e1e229a9bc54c6d40d1147ddd6d7fa9b9b1 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 17:25:04 +0100 Subject: [PATCH 25/39] vault backup: 2025-03-18 17:25:04 --- .obsidian/workspace.json | 4 ++-- Concurrent Systems/notes/6 - Atomicity.md | 8 +++++++- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index b306be6..a8644e3 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -214,10 +214,10 @@ "companion:Toggle completion": false } }, - "active": "88f2e3a5b973712d", + "active": "51157f32453cba69", "lastOpenFiles": [ - "Concurrent Systems/notes/6 - Atomicity.md", "Concurrent Systems/slides/class 6.pdf", + "Concurrent Systems/notes/6 - Atomicity.md", "Concurrent Systems/notes/images/Pasted image 20250318090733.png", "Concurrent Systems/notes/images/Pasted image 20250318090909.png", "Concurrent Systems/slides/class 5.pdf", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index b34c210..7695939 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -69,9 +69,15 @@ 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$ + +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 \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$ From efcd98f2d35caac5160ae2253d40ac52a26ec8dc Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 17:30:04 +0100 Subject: [PATCH 26/39] 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$ From 23b83cbd442f58f35987d00364ec62d9629b8a60 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 17:35:04 +0100 Subject: [PATCH 27/39] vault backup: 2025-03-18 17:35:04 --- .obsidian/workspace.json | 2 +- Concurrent Systems/notes/6 - Atomicity.md | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index b44ffbb..6c1d4f2 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -38,7 +38,7 @@ "file": "Concurrent Systems/slides/class 6.pdf", "page": 6, "left": -23, - "top": 584, + "top": 508, "zoom": 0.6538004750593824 }, "icon": "lucide-file-text", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 24c0ed6..3d3c536 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -73,7 +73,8 @@ $\to'|_X$ $\to|_X$ $\to_X$ -Osservazione: $\to'|_X$ è come dire $\to_{\hat{S}|X}$, infatti l'ordinamento topologico +Osservazione: $\to'|_X$ è come dire $\to_{\hat{S}|X}$. L'ordinamento topologico è letteralmente la sequenza di eventi in S + 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: @@ -83,8 +84,8 @@ $\hat{S}$ is clearly sequential. Moreover: - $\hat{S}_X$ lo storico ottenuto linearizzando $\hat{H}|_X$ - definisce una relazione di ordinamento $\to_X$ - $\hat{S}|_X$ lo storico che ottengo filtrando per le operazioni su X, partendo da $\hat{S}$, che a sua volta viene ottenuto linearizzando $\hat{H}$ - - definisce una relazione di ordinamento $\to|_X$ - - naturlamente, possiamo considerare $\to_X \space = \space <_{\hat{S}_X}$ e $\to|_X \space = \space <_{\hat{S}|_X}$ (se l'ordinamento è uguale, allora anche le coppie in relazione tra loro sono le stesse) + - definisce una relazione di ordinamento $\to|_{\hat{S}_X}$ + - naturlamente, possiamo considerare $\to_X \space = \space <_{\hat{S}_X}$ e $\to|_{\hat{S}_X} \space = \space <_{\hat{S}|_X}$ (se l'ordinamento è uguale, allora anche le coppie in relazione tra loro sono le stesse) > [!PDF|red] class 6, p.6> we would have a cycle of length > > we would contraddict op2 ->x op3 From c41cf3484a486503d1197fe648c5b7651d7a5af0 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 17:40:04 +0100 Subject: [PATCH 28/39] vault backup: 2025-03-18 17:40:04 --- Concurrent Systems/notes/6 - Atomicity.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 3d3c536..d7abe9f 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -73,9 +73,12 @@ $\to'|_X$ $\to|_X$ $\to_X$ -Osservazione: $\to'|_X$ è come dire $\to_{\hat{S}|X}$. L'ordinamento topologico è letteralmente la sequenza di eventi in S +Considero $\to'|_X$ come $\to'$ filtrato per gli eventi su X. -Si ha che $\to|_X \space \subseteq \space \to'|_X$ perché l'ordinamento topologico è letteralmente la sequenza di eventi in $\hat{S}$ +**Osservazione 1:** $\to'|_X$ è come dire $\to_{\hat{S}|X}$ perché l'ordinamento topologico è letteralmente la sequenza di eventi in S, e se filtro entrambi per gli eventi su X ottengo la stessa cosa... + +Considero +Si ha che $\to|_X \space \subseteq \space \to'|_X$ $\hat{S}$ is clearly sequential. Moreover: 1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$, indeed: From 042e391f2c81bc6840df07ecbf164b13bcb57237 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 17:45:04 +0100 Subject: [PATCH 29/39] vault backup: 2025-03-18 17:45:04 --- Concurrent Systems/notes/6 - Atomicity.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index d7abe9f..160cfc2 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -77,7 +77,8 @@ Considero $\to'|_X$ come $\to'$ filtrato per gli eventi su X. **Osservazione 1:** $\to'|_X$ è come dire $\to_{\hat{S}|X}$ perché l'ordinamento topologico è letteralmente la sequenza di eventi in S, e se filtro entrambi per gli eventi su X ottengo la stessa cosa... -Considero +Considero $\to|_X$ come $\to$ filtrato per gli eventi di X. + Si ha che $\to|_X \space \subseteq \space \to'|_X$ $\hat{S}$ is clearly sequential. Moreover: From 0fbc8dc711b7fc22b87500fc1cf7762f0ad9f0f6 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 17:55:04 +0100 Subject: [PATCH 30/39] vault backup: 2025-03-18 17:55:04 --- Concurrent Systems/notes/6 - Atomicity.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 160cfc2..ee9512c 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -77,7 +77,7 @@ Considero $\to'|_X$ come $\to'$ filtrato per gli eventi su X. **Osservazione 1:** $\to'|_X$ è come dire $\to_{\hat{S}|X}$ perché l'ordinamento topologico è letteralmente la sequenza di eventi in S, e se filtro entrambi per gli eventi su X ottengo la stessa cosa... -Considero $\to|_X$ come $\to$ filtrato per gli eventi di 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$ From 0a58fa122d25edcdd2775865e47debe149b7ff4a Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 18:00:04 +0100 Subject: [PATCH 31/39] 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: From cde374481d8122910a23be7128e0082919a9f1a5 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 18:05:04 +0100 Subject: [PATCH 32/39] vault backup: 2025-03-18 18:05:04 --- .obsidian/workspace.json | 4 ++-- Concurrent Systems/notes/6 - Atomicity.md | 18 +++++++++--------- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index c13a352..dbf1fa4 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -36,9 +36,9 @@ "type": "pdf", "state": { "file": "Concurrent Systems/slides/class 6.pdf", - "page": 6, + "page": 7, "left": -23, - "top": 508, + "top": 496, "zoom": 0.6538004750593824 }, "icon": "lucide-file-text", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 36bdd18..a5a782b 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -68,10 +68,7 @@ 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$ +$\hat{S}$ is clearly sequential. Considero $\to'|_X$ come $\to'$ filtrato per gli eventi su X. @@ -81,17 +78,20 @@ Considero $\to|_X$ come $\to$ filtrato per gli eventi di X. Da non confondere co 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$. +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$. Non sono necessariamente uguali perché l'ordinamento topologico può imporre ulteriori ordinamenti tra eventi che in $ non erano esplicitamente vincolati. -$\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}$ - - commento per non diventare scemi: + +Posso quindi dire: $$<_{\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}$$ ricordando: - $\hat{S}_X$ lo storico ottenuto linearizzando $\hat{H}|_X$ - definisce una relazione di ordinamento $\to_X$ - $\hat{S}|_X$ lo storico che ottengo filtrando per le operazioni su X, partendo da $\hat{S}$, che a sua volta viene ottenuto linearizzando $\hat{H}$ - definisce una relazione di ordinamento $\to|_{\hat{S}_X}$ - naturlamente, possiamo considerare $\to_X \space = \space <_{\hat{S}_X}$ e $\to|_{\hat{S}_X} \space = \space <_{\hat{S}|_X}$ (se l'ordinamento è uguale, allora anche le coppie in relazione tra loro sono le stesse) + + +E allora si ha come corollario che$$\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$$ + +Inoltre, dico che, For all p, $\hat{H}|_p=inv(op1_p)res(op1_p)inv(op2_p)res(op2_p$ > [!PDF|red] class 6, p.6> we would have a cycle of length > > we would contraddict op2 ->x op3 From 19d146662e1678b5b9ce2f7738a2687e7d907bf2 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 18:10:04 +0100 Subject: [PATCH 33/39] vault backup: 2025-03-18 18:10:04 --- Concurrent Systems/notes/6 - Atomicity.md | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index a5a782b..9130871 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -91,11 +91,16 @@ Posso quindi dire: $$<_{\hat{S}_X} \space = \space\to_X\space \subseteq\space \s E allora si ha come corollario che$$\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$$ -Inoltre, dico che, For all p, $\hat{H}|_p=inv(op1_p)res(op1_p)inv(op2_p)res(op2_p$ +Inoltre, dico che, For all process p, $\hat{H}|_p=inv(op1_p)res(op1_p)inv(op2_p)res(op2_p)...$, e questo è vero perché lo storico delle operazioni eseguite DA UN SOLO PROCESSO non può non essere sequenziale! + +E siccome +- $op1_p \to_H op2_p \to_H \dots$ +- $\to_H \space \subseteq \space \to'$ + + + + + > [!PDF|red] class 6, p.6> we would have a cycle of length > -> we would contraddict op2 ->x op3 - -... -... - +> we would contraddict op2 ->x op3 \ No newline at end of file From 4cba7cf3fc3213c2768ee2483d40856a8c721a4a Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 18:15:04 +0100 Subject: [PATCH 34/39] vault backup: 2025-03-18 18:15:04 --- Concurrent Systems/notes/6 - Atomicity.md | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 9130871..45e19e0 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -97,10 +97,9 @@ E siccome - $op1_p \to_H op2_p \to_H \dots$ - $\to_H \space \subseteq \space \to'$ +Allora $$\hat{H}|_p = \hat{S}_p$$ +ovverosia, se proiettiamo H e S solo per le operazioni eseguite da un solo processo $p$, allora gli storici saranno uguali. +Infine, si ha che $$\to_H \space \subseteq \space \to \space \subseteq \space \to' \space = \space \to_S$$ - - - -> [!PDF|red] class 6, p.6> we would have a cycle of length -> +> [!PDF|red] class 6, p.6> we would have a cycle of length > > we would contraddict op2 ->x op3 \ No newline at end of file From 9ef252d218c7725796027fe14abed13e8591b9c1 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 18:30:04 +0100 Subject: [PATCH 35/39] vault backup: 2025-03-18 18:30:04 --- Concurrent Systems/notes/6 - Atomicity.md | 1 + 1 file changed, 1 insertion(+) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 45e19e0..e015387 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -99,6 +99,7 @@ E siccome Allora $$\hat{H}|_p = \hat{S}_p$$ ovverosia, se proiettiamo H e S solo per le operazioni eseguite da un solo processo $p$, allora gli storici saranno uguali. + Infine, si ha che $$\to_H \space \subseteq \space \to \space \subseteq \space \to' \space = \space \to_S$$ > [!PDF|red] class 6, p.6> we would have a cycle of length > From 9d0e1a479d535c6d74b54c7f518f0b88a023589e Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 18:35:04 +0100 Subject: [PATCH 36/39] vault backup: 2025-03-18 18:35:04 --- .obsidian/workspace.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index dbf1fa4..cc00233 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -36,9 +36,9 @@ "type": "pdf", "state": { "file": "Concurrent Systems/slides/class 6.pdf", - "page": 7, + "page": 4, "left": -23, - "top": 496, + "top": 152, "zoom": 0.6538004750593824 }, "icon": "lucide-file-text", From b6d023ee588330162c7fe62e172e311b4584d55f Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 18:40:04 +0100 Subject: [PATCH 37/39] vault backup: 2025-03-18 18:40:04 --- Concurrent Systems/notes/6 - Atomicity.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index e015387..3072db6 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -101,6 +101,6 @@ Allora $$\hat{H}|_p = \hat{S}_p$$ ovverosia, se proiettiamo H e S solo per le operazioni eseguite da un solo processo $p$, allora gli storici saranno uguali. Infine, si ha che $$\to_H \space \subseteq \space \to \space \subseteq \space \to' \space = \space \to_S$$ - +perché un ordinamento topologico rispetta tutti i vincoli e quindi lo posso vedere come una linearizzazione. > [!PDF|red] class 6, p.6> we would have a cycle of length > > we would contraddict op2 ->x op3 \ No newline at end of file From 229852c6ddd7aaab9fedbc25dcf790bd1659af07 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 18:45:04 +0100 Subject: [PATCH 38/39] vault backup: 2025-03-18 18:45:04 --- .obsidian/workspace.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index cc00233..b76a4c9 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -218,12 +218,12 @@ }, "active": "681355c2483f6307", "lastOpenFiles": [ - "Concurrent Systems/slides/class 6.pdf", + "Concurrent Systems/notes/5 - Software Transactional Memory.md", "Concurrent Systems/notes/6 - Atomicity.md", + "Concurrent Systems/slides/class 6.pdf", "Concurrent Systems/notes/images/Pasted image 20250318090733.png", "Concurrent Systems/notes/images/Pasted image 20250318090909.png", "Concurrent Systems/slides/class 5.pdf", - "Concurrent Systems/notes/5 - Software Transactional Memory.md", "Concurrent Systems/notes/4c - Dining Philosophers.md", "Concurrent Systems/notes/4 - Semaphores.md", "Concurrent Systems/notes/4b - Monitors.md", From 0551c94f31bb8a798008f6f07be83537d8fc2966 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 19:07:58 +0100 Subject: [PATCH 39/39] vault backup: 2025-03-18 19:07:58 --- .obsidian/workspace.json | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index b76a4c9..1894a1e 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -176,8 +176,8 @@ "state": { "type": "git-view", "state": {}, - "icon": "lucide-file", - "title": "Plugin no longer active" + "icon": "git-pull-request", + "title": "Source Control" } }, { @@ -197,8 +197,7 @@ } ], "direction": "horizontal", - "width": 364.5, - "collapsed": true + "width": 364.5 }, "left-ribbon": { "hiddenItems": {