vault backup: 2025-03-18 16:00:04

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