Posts

Showing posts with the label distributed transactions

Aurora DSQL: Scalable, Multi-Region OLTP

Image
The Aurora DSQL paper finally dropped . Reading it yesterday was an interesting experience, because I spent two years (2022-23) working with the AWS team that designed and built Aurora DSQL. Since I have been very familiar with the architecture, the paper's overview description of the system didn't excite me much. And if I am being honest, reading the paper also felt a bit dry, most likely because I am not doing the usual extra thinking to explore/understand the ideas in the paper. But taking a step back today, and leaving my subjective experience aside, I will try to elaborate on how the DSQL architecture is actually built on a set of aggressive and opinionated engineering bets.  If I had to explain this architecture in a single sentence (just as I used to do for other teams at AWS) it would be this: We took a traditional monolithic database and blew out every single component into an independent, horizontally scalable service. Exploding the Monolith DSQL divides the database ...

TLA+ as a Design Accelerator: Lessons from the Industry

Image
After 15+ years of using TLA+, I now think of it is a design accelerator. One of the purest intellectual pleasures is finding a way to simplify and cut out complexity. TLA+ is a thinking tool that lets you do that. TLA+ forces us out of implementation-shaped and operational reasoning into mathematical declarative reasoning about system behavior. Its global state-transition model and its deliberate fiction of shared memory make complex distributed behavior manageable. Safety and liveness become clear and compact predicates over global state. This makes TLA+ powerful for design discovery. It supports fast exploration of protocol variants and convergence on sound designs before code exists. TLA+ especially shines for distributed/concurrent complex systems. In such systems, complexity exceeds human intuition very quickly. (I often point out to very simple interleaving/nondeterministic execution puzzles to show how much we suck at reasoning about such systems.) Testing is inadequate for su...

Building a Database on S3

Image
Hold your horses, though. I'm not unveiling a new S3-native database. This paper is from 2008. Many of its protocols feel clunky today. Yet it nails the core idea that defines modern cloud-native databases: separate storage from compute. The authors propose a shared-disk design over Amazon S3, with stateless clients executing transactions. The paper provides a blueprint for serverless before the term existed. SQS as WAL and S3 as Pagestore The 2008 S3 was painfully slow, and 100 ms reads weren't unusual. To hide that latency, the database separates "commit" from "apply". Clients write small, idempotent redo logs to Amazon Simple Queue Service (SQS) instead of touching S3 directly. An asynchronous checkpoint by a client applies those logs to B-tree pages on S3 later. This design shows strong parallels to modern disaggregated architectures . SQS becomes the write-ahead log (WAL) and logstore. S3 becomes the pagestore. Modern Aurora follows a similar logic : t...

Tiga: Accelerating Geo-Distributed Transactions with Synchronized Clocks

Image
This paper (to appear at SOSP'25) is one of the latest efforts exploring the dream of a one-round commit for geo-replicated databases. TAPIR tried to fuse concurrency control and consensus into one layer. Tempo and Detock went further using dependency graphs.  Aleksey and I did our usual thing. We recorded our first blind read of the paper. I also annotated a copy while reading, which you can access here . We liked the paper overall. This is a thoughtful piece of engineering, not a conceptual breakthrough. It uses  future timestamps to align replicas  in a slightly new way, and the results are solid. But the presentation needs refinement and stronger formalization. (See our livereading video about how these problems manifested themselves.)  Another study to add to my survey , showing how, with modern clocks, time itself is becoming a coordination primitive. The Big Idea Tiga claims to do strictly serializable one-shot (multi-shot ok with reconnaissance queries t...

Analysing Snapshot Isolation

Image
This paper (PODC'2016) presents a clean and declarative treatment of Snapshot Isolation (SI) using dependency graphs. It builds on the foundation laid by prior work, including the SSI paper we reviewed recently , which had already identified that SI permits cycles with two adjacent anti-dependency (RW) edges, the so-called inConflict and outConflict edges. While the SSI work focused on algorithmic results and implementation, this paper focuses more on the theory (this is PODC after all) of defining a declarative dependency-graph-based model for SI. It strips away implementation details such as commit timestamps and lock management, and provides a purely symbolic framework. It also proves a soundness result (Theorem 10), and leverages the model for two practical static analyses: transaction chopping and robustness under isolation-level weakening. Soundness result and dependency graph model Let's begin with Theorem 10, which establishes both the soundness and completeness of the...

Morty: Scaling Concurrency Control with Re-Execution

Image
This EuroSys '23 paper reads like an SOSP best paper. Maybe it helped that EuroSys 2023 was in Rome. Academic conferences are more enjoyable when the venue doubles as a vacation. The Problem Morty tackles a fundamental question: how can we improve concurrency under serializable isolation (SER), especially without giving up on interactive transactions? Unlike deterministic databases (e.g., Calvin ) that require transactions to declare read and write sets upfront, Morty supports transactions that issue dynamic reads and writes based on earlier results. Transactional systems, particularly in geo-replicated settings, struggle under contention. High WAN latency stretches transaction durations, increasing the window for conflicts. The traditional answer is blind exponential backoff, but that leads to low CPU utilization. TAPIR and Spanner replicas often idle below 17% under contention as Morty's evaluation experiments show. Morty's approach to tackle the problem is to start from...

Chapter 3: Two Phase Locking (Concurrency Control Book)

Image
Chapter 3 presents two-phase locking (2PL). Remember I told you in Chapter 2: Serializability Theory that the discussion is very scheduler-centric? Well, this is a deeper dive into the scheduler, using 2PL as the concurrency control mechanism. The chapter examines the design trade-offs in scheduler behavior, proves the correctness of basic 2PL, dissects how deadlocks arise and are handled, and discusses many variations and implementation issues. Here are the section headings in Chapter 3. Aggressive and Conservative Schedulers Basic Two Phase Locking Correctness of Basic Two Phase Locking Deadlocks Variations of Two Phase Locking Implementation Issues The Phantom Problem Locking Additional Operators Multigranularity Locking Distributed Two Phase Locking Distributed Deadlocks Locking Performance Tree Locking Yep, this is a long chapter: 65 pages.  3.1 Aggressive and Conservative Schedulers The chapter opens by asking: how aggressive or conservative should a scheduler be? An aggress...

Modular verification of MongoDB Transactions using TLA+

Image
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 co...

Popular posts from this blog

The Safest Job from AI may be Writing

The Two Abstractions of System Design: Hide or Reduce

The Agentic Self: Parallels Between AI and Self-Improvement

In Search of a Compositional Theory of Self-Stabilization

Learning about distributed systems: where to start?

Building a Database on S3

Foundational distributed systems papers

Cloudspecs: Cloud Hardware Evolution Through the Looking Glass

Specula: Scaling formal specifications for autonomous model checking of system code

Hints for Distributed Systems Design