Non-interleaving operational semantics for geographically replicated databases

For scalable distributed database systems, weak consistency models are essential. Distributed databases, such as Google Spanner, scale to millions of nodes that replicate data across datacentres possibly located on different continents. At this scale, it is infeasible to maintain serialisability, which assumes that a global total order over committed transactions can be established. Instead, weaker consistency models, such as eventual consistency, causal consistency, sequential consistency and external consistency, are assumed. The problem is that operational models, such as labelled transition systems, tend to assume an interleaving semantics, which serialises transactions. To address this limitation, we provide an operational model that allows a weaker notion of consistency for a geographically distributed database inspired by Spanner. We reduce the timing guarantees provided by Spanner's TrueTime protocol to causal dependencies that are specified in a formal calculus.