20 lines
No EOL
809 B
Markdown
20 lines
No EOL
809 B
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']`.
|
||
|
||
**Def:** a complete history is sequentially consistent if there exists a sequential history $𝑆$ s.t.
|
||
![[Pasted image 20250324082534.png]]
|
||
|
||
![[Pasted image 20250324082545.png]]
|
||
|
||
>[!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}$ |