From 2b88b8deb03971151a349d49e0f07ab508085908 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Tue, 18 Mar 2025 16:45:04 +0100 Subject: [PATCH] vault backup: 2025-03-18 16:45:04 --- Concurrent Systems/notes/6 - Atomicity.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Concurrent Systems/notes/6 - Atomicity.md b/Concurrent Systems/notes/6 - Atomicity.md index 687889b..fe345c0 100644 --- a/Concurrent Systems/notes/6 - Atomicity.md +++ b/Concurrent Systems/notes/6 - Atomicity.md @@ -66,9 +66,11 @@ We now show that $\to$ is acyclic. 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)$$ - +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. Moreover: +1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$. Indeed: > [!PDF|red] class 6, p.6> we would have a cycle of length > > we would contraddict op2 ->x op3