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 (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 a cycle of lenght 2...
       • op2 \to_H op3 entails that inv(op2) <_H res(op3)

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

we would contraddict op2 ->x op3

... ...