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
```