Consistency models lab

The diagram. Three regions — West Europe, East US and Southeast Asia — each with a client and two replicas. The region with the accent border is the write region: every write goes to its leader, which gives it the next log sequence number (LSN) and copies it to every other replica. A replica card shows the LSN it has applied in order, how many versions it is behind, its values of x and y, and badges: gap (it applied a later write before an earlier one — eventual only), waiting (it holds a write until the one before it arrives) and prep (a strong write it has prepared but not yet seen committed). A client card shows its last result, its session token at session level, and in red what was wrong with its last read.

Do something. Change the level at any moment; read or write from any client; read x and y together; cut a region off, fail it, restore it, make another region the write region (a failover); heal the network; switch on a random workload. Tap a client, replica or region on the diagram for the same actions and a few more (pin a read to one replica, delay the next copy to one).

The counters judge every read when it returns: stale (older than a write acknowledged before the read began), went backwards (older than something the same client read before), missed own write, missed a cause (older than a write that came before one the client had already seen), saw a gap, and operations that failed. Latency is shown as p50 and p99 for reads and writes, and acknowledged writes lost in a failover are counted.

Operations lists the latest operations with the replica that served each; Check this run in the history checker sends the whole run there. Replicas shows every replica’s log position; The levels compares what each level promises.

Settings: the starting level, the bound K and T for bounded staleness, the distance between regions, random delay, how long a session replica waits before handing a read to the write region, the client timeout, the write region and the seed.

The store follows Cosmos DB with a single write region (consistency levels, latency and throughput): writes go to one region, which orders them; other regions replicate asynchronously.

The checker tests linearizability by the search of Wing & Gong (1993): repeatedly choose an operation that can go next — one invoked before every unchosen operation has returned — whose observed result fits the register, and backtrack; with Lowe’s (2017) memoisation of (operations chosen, register value) so equivalent states are searched once, as in Porcupine. Each key is checked on its own, which is sound because linearizability is local (Herlihy & Wing, Theorem 1). An operation that never returned may be placed anywhere after its invoke or left out. Sequential consistency (Lamport 1979) is not local, so it is checked over all keys at once by a memoised search over how far each client has got. A smallest failing set is found by dropping operations one at a time (a write together with the reads that saw its value) while the rest still fails, so removing any one more operation makes it pass.

The map is drawn for this page; its structure follows Viotti & Vukolić (2016) and Jepsen’s map of consistency models, and the availability classes follow Bailis et al., Highly Available Transactions (2013). Latency against consistency is Abadi’s PACELC: during a partition, choose availability or consistency; else, latency or consistency.

One write region only. Cosmos DB can also accept writes in every region, where conflicts are resolved by last-writer-wins or a custom procedure, and strong consistency is not offered; that is not simulated (the clocks and CRDTs tool covers merging concurrent writes).

Each region has two replicas; real Cosmos DB partitions hold four per region and use quorums within the region, and strong consistency there uses a dynamic quorum that can leave an unreachable region out. Here a strong write needs every replica, so any partition stops writes.

Latencies are fixed one-way times with optional random delay — no queueing, no request units, no throttling other than the staleness bound. The numbers are illustrative, not measurements of Azure.

A failover is instant and manual; a region that comes back copies the write region’s state, discarding writes that never left it.

The checker handles read, write and compare-and-set registers. It gives up after two million search states (shown as "?"); histories of a few hundred operations per key are fine unless they are very concurrent. Transactions are not checked: for write skew and the isolation levels, use the isolation lab.

Stale, non-monotonic and causal verdicts in the simulator are judged against the write region’s log, which a real client could not see — that is what makes them useful for teaching.