vault backup: 2025-03-19 11:11:04

.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"
 ]

.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",

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