40 lines
No EOL
2.1 KiB
Markdown
40 lines
No EOL
2.1 KiB
Markdown
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)` and `commit(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.
|
||
1. $\forall X : \hat{S}|_X \in semantics(X)$
|
||
2. $S = \{e \in H : e \in t \in committedTrans(\hat{H})\}$
|
||
3. $\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). |