diff --git a/.obsidian/community-plugins.json b/.obsidian/community-plugins.json index 49ffe43..dc1b1be 100644 --- a/.obsidian/community-plugins.json +++ b/.obsidian/community-plugins.json @@ -1,10 +1,9 @@ [ "obsidian-ocr", - "pdf-plus", "obsidian-git", "mathlive-in-editor-mode", "smart-second-brain", "local-gpt", - "obsidian-latex-suite", - "companion" + "companion", + "pdf-plus" ] \ No newline at end of file diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 321ef83..205e276 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -20,8 +20,23 @@ "icon": "lucide-file", "title": "6 - Atomicity" } + }, + { + "id": "3f52278bb3615a8c", + "type": "leaf", + "state": { + "type": "markdown", + "state": { + "file": "conflict-files-obsidian-git.md", + "mode": "source", + "source": false + }, + "icon": "lucide-file", + "title": "conflict-files-obsidian-git" + } } - ] + ], + "currentTab": 1 } ], "direction": "vertical" @@ -194,10 +209,13 @@ "companion:Toggle completion": false } }, - "active": "51157f32453cba69", + "active": "3f52278bb3615a8c", "lastOpenFiles": [ - "Concurrent Systems/slides/class 6.pdf", + "conflict-files-obsidian-git.md", "Concurrent Systems/notes/6 - Atomicity.md", + "Concurrent Systems/notes/images/Pasted image 20250318090909.png", + "Concurrent Systems/notes/images/Pasted image 20250318090733.png", + "Concurrent Systems/slides/class 6.pdf", "Pasted image 20250318090909.png", "Pasted image 20250318090733.png", "Concurrent Systems/slides/class 5.pdf", @@ -230,8 +248,6 @@ "Pasted image 20250305182542.png", "HCIW/notes/1 - UX for IoT.md", "HCIW/exercises/Exercise.md", - "Concurrent Systems/notes/images/Pasted image 20250304082459.png", - "Concurrent Systems/notes/images/Pasted image 20250304093223.png", "Foundation of data science/notes/1 CV Basics.md", "Foundation of data science/notes/7 Autoencoders.md", "Foundation of data science/notes/6 PCA.md", diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 88a40ea..3072db6 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 @@ -31,14 +32,75 @@ $\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}$ -... -> [!PDF|red] class 6, p.6> we would have a cycle of length -> -> we would contraddict op2 ->x op3 +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), 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 $res(op') <_H inv(op)$ + - 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: + - 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, 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 $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)$, 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)inv(op2)res(op2)...$$ +we would have the topological order: $op1\to'op2\to'...$ +$\hat{S}$ is clearly sequential. + +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. 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$. + +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$. Non sono necessariamente uguali perché l'ordinamento topologico può imporre ulteriori ordinamenti tra eventi che in $ non erano esplicitamente vincolati. + + +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 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'$ + +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 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