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

This commit is contained in:
Marco Realacci 2025-03-18 17:30:04 +01:00
parent 9afe2e1e22
commit efcd98f2d3
2 changed files with 8 additions and 5 deletions

View file

@ -6,6 +6,7 @@
{ {
"id": "4c1f5b7a6abb1339", "id": "4c1f5b7a6abb1339",
"type": "tabs", "type": "tabs",
"dimension": 50.63775510204081,
"children": [ "children": [
{ {
"id": "51157f32453cba69", "id": "51157f32453cba69",
@ -26,6 +27,7 @@
{ {
"id": "4ae2dccd2d32173d", "id": "4ae2dccd2d32173d",
"type": "tabs", "type": "tabs",
"dimension": 49.36224489795919,
"children": [ "children": [
{ {
"id": "88f2e3a5b973712d", "id": "88f2e3a5b973712d",
@ -36,8 +38,8 @@
"file": "Concurrent Systems/slides/class 6.pdf", "file": "Concurrent Systems/slides/class 6.pdf",
"page": 6, "page": 6,
"left": -23, "left": -23,
"top": 379, "top": 584,
"zoom": 0.6627078384798101 "zoom": 0.6538004750593824
}, },
"icon": "lucide-file-text", "icon": "lucide-file-text",
"title": "class 6" "title": "class 6"

View file

@ -69,15 +69,16 @@ 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$ $\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}$ Osservazione: $\to'|_X$ è come dire $\to_{\hat{S}|X}$, infatti l'ordinamento topologico
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 \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$