# The Bug in Paxos Made Simple

DevFeed: [The Bug in Paxos Made Simple](<https://devfeed.tech/articles/the-bug-in-paxos-made-simple-12513.md>)

Original publisher: [Read original article](<http://brooker.co.za/blog/2021/11/16/paxos.html>)

Author: Marc Brooker

Published: 2021-11-16T00: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: [distributed-systems](<https://devfeed.tech/topics/distributed-systems.md>), [Algorithms](<https://devfeed.tech/topics/algorithms.md>), [bug](<https://devfeed.tech/topics/bug.md>), [Programming language](<https://devfeed.tech/topics/programming-language.md>), [Stack Overflow](<https://devfeed.tech/topics/stackoverflow.md>)

Tags: [bug](<https://devfeed.tech/tags/bug.md>), [distributed-systems](<https://devfeed.tech/tags/distributed-systems.md>), [programming](<https://devfeed.tech/tags/programming.md>), [programming-language](<https://devfeed.tech/tags/programming-language.md>), [systems](<https://devfeed.tech/tags/systems.md>)

## AI overview

The article explains an apparent bug in the description of Paxos in "Paxos Made Simple," rather than in the Paxos algorithm itself. Using the P programming language's model checker, the author reproduces a failure caused by ambiguities in the paper that can allow a decided value to be forgotten and another value to be chosen, violating Paxos safety.

## Source excerpt

The Bug in Paxos Made Simple There's not really a bug in Paxos, but clickbait is fun. Over the last few weeks, I've been picking up the excellent P programming language, a language for modelling and specifying distributed systems. One of the first things I did in P was implement Paxos - an algorithm I know well, has a lot of subtle failure modes, and is easy to get wrong. Perfect for practicing specification. To test out P's model checker, I intentionally implemented a subtly buggy version of Paxos, following the description in Paxos Made Simple. The model checker found, as expected, implemented the way I read Paxos Made Simple, that Paxos is broken. I mentioned this to a colleague who said they had never heard of this bug. I think it deserves to be more well known, so I thought I'd write a bit about it. The problem lies not in the Paxos algorithm itself, but in the description in the paper. Michael Deardeuff pointed out this bug to me, and also wrote it up in what may be the best Stack Overflow exchange of all time1 (or, at least, the one with the best value-to-upvotes ratio). In the Stack Overflow question, user lambda describes the following sequence of events: Consider that there are totally 3 acceptors ABC. We will use X(n:v,m) to denote the status of acceptor X: proposal n:v is the largest numbered proposal accepted by X where n is the proposal number and v is the value of the proposal, and m is the number of the largest numbered prepare request that X has ever responded. The following can play out: 1. P1 sends 'prepare 1' to AB 2. Both AB respond P1 with a promise to not to accept any request numbered smaller than 1.\ Now the status is: A(-:-,1) B(-:-,1) C(-:-,-) 3. P1 receives the responses, then gets stuck and runs very slowly 4. P2 sends 'prepare 100' to AB 5. Both AB respond P2 with a promise to not to accept any request numbered smaller than 100. Now the status is: A(-:-,100) B(-:-,100) C(-:-,-) 6. P2 receives the responses, chooses a value b and sends '