vault backup: 2025-03-18 17:25:04
This commit is contained in:
parent
bf1a229fa5
commit
9afe2e1e22
2 changed files with 9 additions and 3 deletions
4
.obsidian/workspace.json
vendored
4
.obsidian/workspace.json
vendored
|
@ -214,10 +214,10 @@
|
||||||
"companion:Toggle completion": false
|
"companion:Toggle completion": false
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
"active": "88f2e3a5b973712d",
|
"active": "51157f32453cba69",
|
||||||
"lastOpenFiles": [
|
"lastOpenFiles": [
|
||||||
"Concurrent Systems/notes/6 - Atomicity.md",
|
|
||||||
"Concurrent Systems/slides/class 6.pdf",
|
"Concurrent Systems/slides/class 6.pdf",
|
||||||
|
"Concurrent Systems/notes/6 - Atomicity.md",
|
||||||
"Concurrent Systems/notes/images/Pasted image 20250318090733.png",
|
"Concurrent Systems/notes/images/Pasted image 20250318090733.png",
|
||||||
"Concurrent Systems/notes/images/Pasted image 20250318090909.png",
|
"Concurrent Systems/notes/images/Pasted image 20250318090909.png",
|
||||||
"Concurrent Systems/slides/class 5.pdf",
|
"Concurrent Systems/slides/class 5.pdf",
|
||||||
|
|
|
@ -69,9 +69,15 @@ This said, we can say that **every DAG admits a topological order** (a total ord
|
||||||
Let us define a linearization of $\hat{H}$ as follows: $$\hat{S}=inv(op1)res(op1)inv(op2)res(op2)...$$
|
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'...$
|
we would have the topological order: $op1\to'op2\to'...$
|
||||||
|
|
||||||
|
$\to'_X$
|
||||||
|
$\to|_X$
|
||||||
|
$\to_X$
|
||||||
|
|
||||||
|
Si ha che $\to|_X \space \subseteq \space \to'_X$ perché l'ordinamento topologico è letteralmente la sequenza di eventi in $\hat{S}$
|
||||||
|
|
||||||
$\hat{S}$ is clearly sequential. Moreover:
|
$\hat{S}$ is clearly sequential. Moreover:
|
||||||
1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$, indeed:
|
1. $\forall X :\hat{S}|_{X} = \hat{S}_X (\in semantics(X))$, indeed:
|
||||||
- $<_{\hat{S}_X} \space = \space\to_X\space \subseteq\space \to'_X\space = \space\to_{\hat{S}|X}\space=\space<_{\hat{S}|X}$
|
- $<_{\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}$
|
||||||
- commento per non diventare scemi:
|
- commento per non diventare scemi:
|
||||||
- $\hat{S}_X$ lo storico ottenuto linearizzando $\hat{H}|_X$
|
- $\hat{S}_X$ lo storico ottenuto linearizzando $\hat{H}|_X$
|
||||||
- definisce una relazione di ordinamento $\to_X$
|
- definisce una relazione di ordinamento $\to_X$
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue