diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 86f3ea4..d54f470 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -32,6 +32,7 @@ $\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}$ @@ -43,7 +44,8 @@ We now show that $\to$ is acyclic. - 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 $r$ + - 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. > [!PDF|red] class 6, p.6> we would have a cycle of length