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$