2.1 KiB
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'], thenres[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.
!
!
there is another linearization possible! I can also push a before if I pull it before c!
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})
Let \to denote \to_{H} \cup \bigcup_{X \in H} \to _{X}
...
[!PDF|red] class 6, p.6> we would have a cycle of length
we would contraddict op2 ->x op3
... ...