2 KiB
Let us define op ->_{proc} op' to hold whenever there exists a process p that issues both operations with res[op] happening before inv[op'].
Sequential consistency
Def: a complete history is sequentially consistent if there exists a sequential history 𝑆 s.t.
!
!
Warning
The problem with sequential consistency is that it is NOT compositional.
Consider for example the following two processes:
p1: Q.enq(a); Q'.enq(b'); Q'deq()->b'
p2: Q'.enq(a'); Q.enq(b); Q.deq()->b
In isolation, both processes are sequentially consistent.
However, no total order on the previous 6 operations respects the semantics of a queue:
- if p1 receives b' from Q'.deq, we have that Q'.enq(a'), must arrive after Q'.enq(b')
- to respect \to_{proc}, also the remaining behavior of p2 must arrive after
- hence, Q.enq(a) arrived before Q.enq(b) and so it is not possible for p2 to receive b from its Q.deq.
Hence, we have two histories that are sequentially consistent but whose composition cannot be sequentially consistent \to no compositionality!
Serializability
(typical notion in databases)
- instead of processes, we have transactions
- consequently, we have also two other kinds of events:
abort(t)andcommit(t)- in every history, we have at most one of these events for every transaction
- if the history is complete, we must have exactly one of these events for transaction
- a sequential history is formed by committed transactions only
Def: a complete history \hat{H} is serializable if there exists a sequential history \hat{S} s.t.
\forall X : \hat{S}|_X \in semantics(X)S = \{e \in H : e \in t \ in committedTrans(\hat{H})\}\to_{trans} \subseteq \to_{S}where\to_{trans}is defined like\to_{proc}in sequential consistency.
It is a more general notion than linearizability, but it is not compositional (consider the previous example but with transactions instead of processes).