Context

This is why you need to learn about MySQL server metrics, especially InnoDB metrics:

Context

This is why you need to learn the basics of MySQL replication, especially the cause of replication lag:

Context

This is why you need to learn about MySQL transactions and data locks, which are closely related:

Context

This is why you need to learn about common challenges when using MySQL:

Key Points

• Split-brain occurs when two or more MySQL instances in the same replication topology are written to
• Split-brain is a detriment to data integrity—the data can no longer be trusted
• Data drift occurs when a replica becomes out of sync with the source
• Data drift is real but the origin of the drift is virtually impossible to pinpoint
• Data drift can be detected with pt-table-checksum
• ORMs can generate very poor queries and overall performance
• Schemas always change, so an online schema change (OSC) tool is must-have
• There are three popular OSC tools: pt-online-schema-change, gh-ost, and Spirit
• MySQL has non-standard SQL statements, options, and clauses
• Applications do not fail gracefully by default; it takes effort to fail gracefully
• High performance MySQL is difficult

Pitfalls

• Not taking into account the key points above

Hack MySQL Articles

• The Future of MySQL Schema Change: Spirit
• How Not to Use MySQL
• When MySQL Goes Away

Additional Resources

Context

This is why you need to learn about the reality of using MySQL in the cloud:

Chapter 2 of Concurrency Control and Recovery in Database Systems (1987) by Bernstein, Hadzilacos, and Goodman is a foundational treatment of serializability theory. It is precise, formal, yet simple and elegant, a rare combination for foundational theory in a systems domain. Databases got lucky here: serializability theory is both powerful and clean.

The chapter builds up the theory step by step, introducing:

1. Histories
2. Serializable histories
3. The Serializability Theorem
4. Recoverability and its variants
5. Generalized operations beyond reads/writes
6. View equivalence

Each section motivates definitions clearly, presents tight formalism, and illustrates ideas with well-chosen examples.

2.1 Histories

This section lays the groundwork. It starts slow, and doesn't do anything fancy. It first defines what it means for the operations within a transaction to form a well-founded partial order. This intra-transaction ordering extends naturally to inter-transaction operations, forming a superset relation. Building on this, the book then defines a history as a partial order over operations from a set of transactions. Operations include reads (r₁[x]), writes (w₁[x]), commits (c₁), and aborts (a₁). Here the subscripts denote these operations all belong to transaction T₁. A history models the interleaving of these operations from different transactions, respecting the per-transaction order and ensuring all conflicting operations are ordered.

The abstraction here is elegant. The model omits values, conditionals, assignments, anything not visible to the scheduler. Only the structure of dependencies matters. This minimalism is a strength: it gives just enough to reason about correctness. The section is also careful to handle incomplete histories (i.e., prefixes), which is crucial for modeling crashes and recovery.

The discussion is very scheduler-centric. Since the scheduler is the component responsible for enforcing serializability, the model is tailored to what the scheduler can observe and act on. But this leads to missed opportunities as I mention below in Section 2.6 View equivalence.

2.2 Serializable Histories

This is where things get real. The goal is to define when a concurrent execution (history) is “as good as” some serial execution. The section has a simple game plan:  define equivalence between histories (conflict equivalence), define serial histories, and finally say a history is serializable if it is equivalent to some serial history.

The chapter introduces the serialization graph (SG). Nodes are committed transactions. Edges capture conflicts: if T_i writes x before T_j reads or writes x, we add an edge T_i → T_j.

The formalism is tight, but not heavy. A good example is Fig 2-1 (p. 30), which compares equivalent and non-equivalent histories. (Minor typo: second w₁[x] in H₃ should be w₁[y].)

Theorem 2.1 (Serializability Theorem): A history is serializable iff its serialization graph is acyclic.

That's a beautiful punchline: serializability reduces to a cycle check in the conflict graph.

Credit is where it is due. In this case it is Jim Gray again! At the end of the section there is an acknowledgment stating that: The definition of equivalence and serializability used here and the Serializability Theorem are from "Gray, J.N., Lorie, R.A., Putzulo, G.R., Traiger, I.L. Granularity of Locks and Degrees of Consistency in a Shared Database. Research Report, IBM, September, 1975." 

2.3 The Serializability Theorem

This section proves the big theorem about equivalence to a serial execution.

Intuitively, if SG(H) is acyclic, we can topologically sort it into a serial history equivalent to H. And if SG(H) has a cycle, then H cannot be serialized.

The figure shows an example. Edges in SG(H) constrain any valid serial order. A cycle means contradictory constraints, and hence, no valid serial order.

2.4 Recoverable Histories

Serializability ensures correctness in a crash-free world. But in practice, systems crash, transactions abort, and partial executions matter. To account for faults, this section defines increasingly strict notions:

Recoverable (RC): If T_j reads from T_i, then T_i must commit before T_j.

Avoids Cascading Aborts (ACA): T_j can only read from committed transactions.

Strict (ST): Reads and overwrites can happen only after the previous writer commits or aborts.

Theorem 2.2: ST ⊂ ACA ⊂ RC

The inclusion hierarchy is illustrated in Fig 2-2. The intersection of these properties with SR defines realistic schedules that can tolerate failures and support recovery.

Note that RC, ACA, and ST are prefix commit-closed properties, that is if they hold for history H, they also hold for any prefix of H. Nice and clean.

2.5 Operations Beyond Reads and Writes

I was happy to see this section. The authors show how the theory generalizes to operations beyond reads and writes, as long as we redefine the notion of conflict appropriately.

Two operations conflict if the order in which they execute affects: the final state of the database, or the values returned by operations. Fig. 2-3 gives the compatibility matrix to capture conflict relations between Read/Write/Inc/Dec. Increment(x) adds 1 to data item x and Decrement(x) subtracts 1 from x. An Inc or Dec does not return a value to the transaction that issues it.

The example history H₁₁ shows how to construct SG(H) even with these new operations. The theory lifts cleanly. Since SG(H_11) is acyclic, the generalized Serializability Theorem says that H_11 is SR. It is equivalent to the serial history T1 T3 T2 T4 which can be obtained by topologically sorting SG(H_11). DAGs FTW!

Still, this is a limited discussion. It's not expressive enough to model more general commutativity. But the seeds of CRDTs are here. In CRDTs, you model operations based on whether they commute under all interleavings. There is an on-going research direction trying to build a nice theory around more general operations and monotonicity concepts.

2.6 View Equivalence

This section introduces view serializability (VSR), a more permissive alternative to conflict serializability. Two histories are view equivalent if:

• Every read in one history reads from the same write as in the other.
• The final write to each data item is the same in both histories.

VSR allows more schedules than CSR. Consider the example below. T3 overwriting both x and y saves the day and masks the conflicts in T1 and T2. Interesting special case!

The book says that testing for VSR is NP-complete, and that kills its usefulness for schedulers. The authors argue that all practical schedulers use conflict serializability, and  view serializability is too expensive to enforce. Yet they acknowledge it’s conceptually useful, especially for reasoning about multicopy databases (Chapters 5 and 8).

Reading this section, I had an interesting question. Is view serializability the same as client-centric consistency? They seem very similar. Client-centric consistency, as discussed in Crooks et al., PODC 2017, defines correctness in terms of what reads observe. VSR is similarly observational.

So while VSR wasn’t practical for scheduling, it found a second life in defining observational consistency in distributed systems. I think there's more fruit on this tree.

Almost a year ago, we launched our company with our “Ode to Postgres”, with the goal of making the fruits of the highly successful Umbra research project available to you and everyone else. Umbra was created to incorporate all the lessons learned from the first 40 years of database systems into a new system built from the ground up to take advantage of modern hardware such as multi-core CPUs, fast SSDs, and cloud storage.

Joint work with Will Schultz.

A transaction groups multiple operations into an all-or-nothing logical-box to reduce the surface area exposed to concurrency control and fault recovery, simplifying the application programmer's job. Transactions support ACID guarantees: atomicity, consistency, isolation, durability. Popular isolation levels include, Read Committed (RC), Snapshot Isolation (SI), and Serializability (SER), which offer increasing protection against concurrency anomalies.

MongoDB Transactions

MongoDB’s transaction model has evolved incrementally.  

• v3.2 (2015): Introduced single-document transactions using MVCC in the WiredTiger storage engine.  
• v4.0 (2018): Extended support to multi-document transactions within a replica set (aka shard).  
• v4.2 (2019): Enabled fully distributed transactions across shards.

Replica Set Transactions. All transaction operations are first performed on the primary using the WiredTiger transaction workflow/algorithm. Before commit of the transaction, all the updates are Raft-replicated with secondaries using the assigned timestamp to ensure consistent ordering. MongoDB uses Hybrid Logical Clocks (HLCs). The read timestamp reflects the latest stable snapshot. The commit timestamp is issued atomically and advances the cluster time. The default ReadConcern="Snapshot" ensures reads reflect a majority-committed snapshot with a given timestamp without yielding. And the WriteConcern="Majority" guarantees writes are durably replicated to a majority.

Distributed Transactions. MongoDB txns are general interactive transactions, rather than limited one-shot transactions as in DynamoDB. Clients interact through mongos, the transaction router, for executing a transaction. Mongos assigns the transaction a cluster-wide read timestamp and dispatches operations to relevant shard primaries. Each shard primary sets its local WiredTiger read timestamp and handles operations. If a conflict (e.g., write-write race) occurs, the shard aborts the transaction and informs mongos.

If the transaction is not aborted and the client asks for a commit, the mongos asks the first shard contacted for the transaction to coordinate the 2-phase commit (2PC). Handing off the commit-coordination to a Raft-replicated primary helps ensure durability/recoverability of the transaction. The shard primary launches a standard 2PC:

• Sends "prepare" to all participant shards.
• Each shard Raft-replicates a prepare oplog entry with a local prepare timestamp.
• The coordinator picks the max prepare timestamp returned from the shards as the global commit timestamp.
• Participant shards Raft-replicate commit at this timestamp and acknowledge back.

Using Alex Miller's Execution, Validation, Ordering, Persistence (EVOP) framework to describe MongoDB's distributed transactions, we get the following figure. MongoDB overlaps execution and validation. Execution stages local changes at each participant shard. All the while, Validation checks for write-write and prepare conflicts. Ordering and Persistence come later. The global commit timestamp provides the ordering for the transactions. Shards expose changes atomically using this timestamp.

MongoDB provides an MVCC+OCC flavor that prefers aborts over blocking. WiredTiger acquires locks on keys at first write access, causing later conflicting transactions to abort. This avoids delays from waiting, reducing contention and improving throughput under high concurrency.

TLA+ Modeling

Distributed transactions are difficult to reason about. MongoDB’s protocol evolved incrementally, tightly coupling the WiredTiger storage layer, replication, and sharding infrastructure. Other sources of complexity include aligning time across clusters, speculative majority reads, recovery protocol upon router failure, chunk migration by the catalog,  interactions with DDL operations, and fault-tolerance.

To reason about MongoDB's distributed transaction protocol formally, we developed the first TLA+ specification of multi-shard database transactions at scale. Our spec is available publicly on GitHub. This spec captures the transaction behavior and isolation guarantees precisely.

Our TLA+ model is modular. It consists of MultiShardTxn, which encodes the high-level sharded transaction protocol, and Storage, which models replication and storage behavior at each shard. This modularity pays off big-time as we discuss in the model-based verification section below.

We validate isolation using a state-based checker based on the theory built by Crooks et al., PODC’17 and the TLA+ library implemented by Soethout. The library would take a log of operations and verify whether the transactions satisfy snapshot isolation, read committed, etc. This is a huge boost for checking/validating transaction isolation.

Our TLA+ model helps us explore how RC/WC selection for MongoDB tunable consistency levels affect transaction isolation guarantees. As MongoDB already tells its customers,  MongoDB's "ReadConcern: majority" does not guarantee snapshot isolation. If you use it instead of "ReadConcern:Snapshot", you may get fractured reads: a transaction may observe some, but not all, of another transaction's effects.

Let's illustrate this with a simplified two-shard, two-transaction model from an earlier spec. T1 writes to K1 and K2 (sharded to S1 and S2, respectively) and commits via two-phase commit. T2 reads K1 before T1 writes it and K2 after T1 has committed. Due to `readConcern: majority`, it reads the old value of K1 and the new value of K2, violating snapshot isolation. The read is fractured.

You can explore this violation trace using a browser-based TLA+ trace explorer that Will Schultz built by following this link. The Spectacle tool loads the TLA+ spec from GitHub, interprets it using JavaScript interpreter, and shows/visualizes step-by-step state changes. You can step backwards and forwards using the buttons, and explore enabled actions. This makes model outputs accessible to engineers unfamiliar with TLA+. You can share a violation trace simply by sending a link.

Modeling helped us to clarify another subtlety: handling prepared but uncommitted transactions in the storage engine. If the transaction protocol ignores a prepare conflict, T2's read at the t-start snapshot might see a value that appears valid at its timestamp, but is later overwritten by T1's commit at an earlier timestamp, violating snapshot semantics. That means a read must wait on prepared transactions to avoid this problem. This is an example of cross-layer interaction between the transaction protocol and the underlying WiredTiger storage we mentioned earlier.

Finally, some performance stats. Checking Snapshot Isolation and Read Committed with the TLA+ model on an EC2 `m6g.2xlarge` instance takes around 10 minutes for small instances of the problem. With just two transactions and two keys, the space is large but manageable. Bugs, if they exist, tend to show up even in small instances.

Model-based Verification

We invested early in modularizing the storage model (a discipline Will proposed) which paid off. With a clean storage API between the transaction layer and storage engine, we can generate test cases from TLA+ traces that exercise the real WiredTiger code, not just validate traces. This bridges the gap between model and implementation.

WiredTiger, being a single-node embedded store with a clean API, is easy to steer and test. We exploit this by generating unit tests directly from the model. Will built a Python tool that:

• Parses the state graph from TLC,
• Computes a minimal path cover,
• Translates each path into Python unit tests,
• Verifies that implementation values conform to the model.

This approach is powerful: our handwritten unit tests number in the thousands, but the generator produces over 87,000 tests in 30 minutes. Each test exercises the precise contract defined in the model, systematically linking high-level protocol behavior to the low-level storage layer. These tests bridge model and code, turning formal traces into executable validations.

Permissiveness

We use TLA+ to also evaluate the permissiveness of MongoDB’s transaction protocol—the degree of concurrency it allows under a given isolation level without violating correctness. Higher permissiveness translates to fewer unnecessary aborts and better throughput. Modeling lets us quantify how much concurrency is sacrificed for safety, and where the implementation might be overly conservative.

To do this, we compare our protocol's accepted behaviors to abstract commit tests from Crooks et al PODC'17 paper. By comparing the transaction protocol behavior to idealized isolation specs, we can locate overly strict choices and explore safe relaxations.

For example, for read committed, MongoDB's transaction protocol (computed over our finite model/configurations) accepts around 76% of the behaviors allowed by the isolation spec. One source of restriction for Read Committed is prepare conflicts, a mechanism that prevents certain races. Disabling it raises permissiveness to 79%. In one such case, a transaction reads the same key twice and sees different values: a non-repeatable read. Snapshot isolation forbids this;  but read committed allows it. MongoDB blocks it, maybe unnecessarily. If relaxing this constraint improves performance without violating correctness, it may be worth reconsidering.

Future Work

Our modular TLA+ specification brings formal clarity to a complex, distributed transaction system. But work remains on the following fronts:

• Model catalog behavior to ensure correctness during chunk migrations.
• Extend multi-grain modeling to other protocols.
• Generate test cases directly from TLA+ to bridge spec and code.
• Analyze and optimize permissiveness to improve concurrency.

I'm catching up on Phil Eaton's book club and just finished the preface and Chapter 1 of Concurrency Control and Recovery in Database Systems by Bernstein, Hadzilacos, and Goodman.

This book came out in 1987: two years before the fall of Berlin wall, 5 years before Windows 3.1, and before the Gray/Reuters book on Transaction Processing. 

I was first surprised about why "Recovery" was featured prominently in the book title, but then realized that in 1987 there was no solid solution for recovery. The ARIES paper on the write-ahead-log came out in 1992.

Once I realized that, the structure made sense: concurrency control (Chapters 1–5), recovery (Chapters 6–7), and a forward-looking chapter on replication (Chapter 8), where they candidly admit: "No database systems that we know of support general purpose access to replicated distributed data."

1. The Problem
2. Serializability Theory
3. Two Phase Locking
4. Non-Locking Schedulers
5. Multiversion Concurrency Control
6. Centralized Recovery
7. Distributed Recovery
8. Replicated Data

Chapter 1: The Problem

Chapter 1 motivates the twin problems of concurrency control and recovery. It defines correct transaction behavior from the user’s point of view and introduces an internal system model that will be used throughout the book.

"User's point of view" here means an operational one, focused on histories of reads/writesm rather than the state-based, client-centric view I am fond of. (See my write-up of Seeing is Believing, Crooks et al., PODC 2017.)

With 40 years of hindsight, the definitions in Chapter 1 reads as straightforward: transactions, commit/abort, recoverability, cascading aborts, lost updates, serializability. The chapter uses many scenarios to illustrate how transactions interfere and how their effects must sometimes be undone upon abort.

I was initially surprised by the level of detail around undoing writes, until I remembered that this is a single-version model. No MVCC yet. Chapter 5 eventually gets there, explaining its benefits and trade-offs. But in 1987, MVCC was too costly in terms of storage/CPU, and OCC was not considered due to high contention workloads of that era. Instead, transactions were implemented with 2PL on resource-constrained single computers. Bernstein himself contributed a lot for the popularization of both MVCC and OCC.

The chapter closes with a model of a database system with four components: transaction manager (TM), scheduler, recovery manager (RM), and cache manager (CM). Transactions issue operations to the TM, which forwards them to the scheduler for concurrency control. The scheduler ensures serializability (and often strictness) by delaying, executing, or rejecting operations. The RM guarantees atomicity and durability, and uses Fetch/Flush from the CM to read/write persistent state. The CM handles movement between volatile and stable storage.

Coordination among modules relies on handshaking: if a module wants two operations ordered (say, write before flush), it must wait for an acknowledgment before issuing the next operation. This is a minimalist model of layered interaction that earns points for clarity and separation of concerns, although real systems today bear little resemblance to it.

 This post has benchmark results for RocksDB 10.x, 9.x, 8.11, 7.10 and 6.29 on a large server.

\tl;dr

• There are several big improvements
• There are no new regressions
• For the block cache hyperclock does much better than LRU on CPU-bound tests