vault backup: 2025-03-18 15:30:04

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