master-degree-notes/Concurrent Systems/notes/6 - Atomicity.md

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.

!

! 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 be 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, this implies res(op') <_X inv(op), which means that op' \to_X op, and so \to_X would be cyclic.

[!PDF|red] class 6, p.6> we would have a cycle of length

we would contraddict op2 ->x op3

... ...