1.6 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.
!
!