# Exploring TLA+ with two-phase commit

DevFeed: [Exploring TLA+ with two-phase commit](<https://devfeed.tech/articles/exploring-tla-with-two-phase-commit-12447.md>)

Original publisher: [Read original article](<http://brooker.co.za/blog/2013/01/20/two-phase.html>)

Author: Marc Brooker

Published: 2013-01-20T00:00:00Z

Content type: article

Language: en

Sources: [Marc Brooker's Blog](<https://devfeed.tech/sources/marc-brooker-s-blog.md>), [Marc Brooker's Blog](<https://devfeed.tech/sources/marc-brooker-s-blog-2.md>)

Topics: [Algorithms](<https://devfeed.tech/topics/algorithms.md>), [Database](<https://devfeed.tech/topics/database.md>), [Transactions](<https://devfeed.tech/topics/transactions.md>), [systems](<https://devfeed.tech/topics/systems.md>)

Tags: [algorithms](<https://devfeed.tech/tags/algorithms.md>), [database](<https://devfeed.tech/tags/database.md>), [systems](<https://devfeed.tech/tags/systems.md>), [transactions](<https://devfeed.tech/tags/transactions.md>)

## AI overview

An introduction to modeling and testing the two-phase commit atomic commit protocol with TLA+. The article explains how the protocol coordinates changes across multiple database systems so a transaction is either applied everywhere or nowhere, while highlighting subtle failure modes and the difficulty of reasoning about distributed behavior.

## Source excerpt

Exploring TLA+ with two-phase commit Using testable pseudocode to test a distributed algorithm There are very few distributed algorithms more widely known by working programmers than the two-phase commit atomic commit protocol. It's a great algorithm to use for teaching purposes: two-phase commit is both extremely simple to write down, and has significant caveats. Some of these shortcomings are obvious, and easily noticed by most students, and some are much more subtle. At a high level, two-phase commit is an atomic commit protocol: it ensures that changes across multiple database systems are either applied to all the systems or to none of them. Assuming a serial stream of transactions, two-phase commit ensures atomicity - the transaction is either fully applied or not applied at all. A single coordinator (let's call her Alice) runs a group of fried chicken restaurants, and wants each restaurant manager (the literature calls them cohorts, let's them Bob and Chuck) to paint their green restaurant blue. Alice really cares that her customers get a consistent fried chicken experience, so wants to make sure that all the managers do the work or none of them to do it. If Alice simply asked Bob to do the work, then asked Chuck, she'd be in trouble. If Bob went ahead and did the work, then Chuck couldn't (say he didn't have enough paint), Alice would need to ask Bob undo his work. If Bob was then out of green paint, Alice would be stuck with inconsistent restaurant colors. In Alice's world, that's a catastrophe. Instead, Alice uses two-phase commit. First, she calls Bob and Chuck and asks them to check if they can repaint today. When both acknowledge they can, Alice calls them and asks them to go ahead. For this to work, she doesn't have to get both of them on the same conference call. She just needs to call them one after the other. Alice also needs to be sure that Bob and Chuck won't lie to her about being able to do the work, and that Bob and Chuck will keep answering the