99 lines
6.1 KiB
Markdown
99 lines
6.1 KiB
Markdown
We have a set of n sequential processes $p_{1},...,p_n$ , that access $m$ concurrent objects $X_1,...,X_m$ by invoking operations on the form `Xi.op(args)(ret)`.
|
||
|
||
When invoked by $p_j$, the invocation `Xi.op(args)(ret)` is modeled by two events: `inv[Xi.op(args) by pj]` and `res[Xi.op(ret) to pj]`.
|
||
|
||
A **history** (or **trace**) is a pair $\hat{H}=(H, <_{H})$ where $H$ is a set of events and $<_{H}$ is a total order on them.
|
||
|
||
The *semantics* (of systems and/or objects) will be given as the set of traces.
|
||
|
||
A history is **sequential** if it is of the form `inv res inv res ... inv res inv inv inv ...`, where every res is the result of the immediately preceding inv. (The last invocations do not have a return).
|
||
A sequential history can be represented as a sequence of operations.
|
||
|
||
A history is **complete** if every inv is eventually followed by a corresponding res, it is **partial** otherwise.
|
||
|
||
### Linearizability
|
||
A complete history $\hat{H}$ is **linearizable** if there exists a sequential history $\hat{S}$ s.t.
|
||
- $\forall X :\hat{S}|_{X} \in semantics(X)$
|
||
- $\forall p:\hat{H}|_{p} = \hat{S}|_p$
|
||
- cannot swap actions performed by the same process
|
||
- If $res[op] <_{H} inv[op']$, then $res[op] <_{S} inv[op']$
|
||
- can rearrange events only if they overlap
|
||
|
||
Given an history $\hat{K}$, we can define a binary relation on events $⟶_{K}$ s.t. (op, op’) ∈ ⟶K if and only if res[op] <K inv[op’]. We write op ⟶K op’ for denoting (op, op’) ∈ ⟶K. Hence, condition 3 of the previous Def. requires that ⟶H ⊆ ⟶S.
|
||
|
||
![[Pasted image 20250318090733.png]]
|
||
|
||
![[Pasted image 20250318090909.png]]But there is another linearization possible! I can also push a before if I pull it before c!
|
||
Of course I have to respect the semantics of a Queue (if I push "a" first, I have to pop "a" first because it's a fucking FIFO)
|
||
|
||
#### Compositionality theorem
|
||
$\hat{H}$ is linearizable if $\hat{H}|_{X}$ is linearizable, for all X in H
|
||
(it is good to linearize complex traces)
|
||
|
||
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}$
|
||
|
||
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), 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 $res(op') <_H inv(op)$
|
||
- Since $\hat{S}_X$ is a linearization of $\hat{H}|_X$ and op/op' are on X (literally because we have op ->x op'), this implies $res(op') <_X inv(op)$, which means that $op' \to_X op$, and so it won't be a total order... So this is not possible either.
|
||
|
||
3. It cannot have cycles with more than 2 edges:
|
||
- by contradiction, consider a shortest cycle
|
||
- adjacent edges cannot belong to the same order (e.g. not both $\to_X$), otw. the cycle would be shortable, because of transitivity of the total order!
|
||
- adjacent edges cannot belong to orders on different objects
|
||
- this would mean that an operation is involved in both $\to_X$ and $\to_Y$ but it is not possible of course, so the cycle can only happen edges in $\to_X$ and $\to_H$.
|
||
- Hence, at least one $\to_X$ exists and it must be between two $\to_H$ i.e.: $$op1 \to_H op2 \to_X op3 \to_H op4$$, likely with op1 = op4
|
||
- can this be a cycle?
|
||
- $op1 \to_H op2$ means that $res(op1) <_H inv(op2)$
|
||
- $op2 \to_X op3$ entails that $inv(op2) <_H res(op3)$
|
||
- if not, as is a total order, we would have that $res(op3) <_H inv(op2)$, but we then would have $op3 \to_H op2$, forming a cycle of lenght 2 because $op2 \to_X op3$, and we know cycles of lenght 2 are not possible...
|
||
- $op3 \to_H op4$ means that $res(op3) <_H inv(op4)$
|
||
|
||
- We would then have that $res(op1) <_H inv(op2) <_H res(op3) <_H inv(op4)$
|
||
- So by transitivity $res(op1) <_H inv(op4)$, i.e. $op1 \to_H op4$
|
||
- IN CONTRADICTION WITH HAVING CHOSEN A SHORTEST CYCLE
|
||
- as if op4 = op1, then this could not happen as $\to$ is a total order.
|
||
|
||
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)inv(op2)res(op2)...$$
|
||
we would have the topological order: $op1\to'op2\to'...$
|
||
|
||
$\to'|_X$
|
||
$\to|_X$
|
||
$\to_X$
|
||
|
||
Considero $\to'|_X$ come $\to'$ filtrato per gli eventi su X.
|
||
|
||
**Osservazione 1:** $\to'|_X$ è come dire $\to_{\hat{S}|X}$ perché l'ordinamento topologico è letteralmente la sequenza di eventi in S, e se filtro entrambi per gli eventi su X ottengo la stessa cosa...
|
||
|
||
Considero $\to|_X$ come $\to$ filtrato per gli eventi di X.
|
||
|
||
Si ha che $\to|_X \space \subseteq \space \to'|_X$
|
||
|
||
$\hat{S}$ is clearly sequential. Moreover:
|
||
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}$
|
||
- commento per non diventare scemi:
|
||
- $\hat{S}_X$ lo storico ottenuto linearizzando $\hat{H}|_X$
|
||
- definisce una relazione di ordinamento $\to_X$
|
||
- $\hat{S}|_X$ lo storico che ottengo filtrando per le operazioni su X, partendo da $\hat{S}$, che a sua volta viene ottenuto linearizzando $\hat{H}$
|
||
- definisce una relazione di ordinamento $\to|_{\hat{S}_X}$
|
||
- naturlamente, possiamo considerare $\to_X \space = \space <_{\hat{S}_X}$ e $\to|_{\hat{S}_X} \space = \space <_{\hat{S}|_X}$ (se l'ordinamento è uguale, allora anche le coppie in relazione tra loro sono le stesse)
|
||
> [!PDF|red] class 6, p.6> we would have a cycle of length
|
||
>
|
||
> we would contraddict op2 ->x op3
|
||
|
||
...
|
||
...
|
||
|