1.5 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