HackerPapers

arXiv:1906.10917cs.DC

On the correctness of Egalitarian Paxos

Pierre Sutra

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

Abstract

This paper identifies a problem in both the TLA+ specification and the implementation of the Egalitarian Paxos protocol. It is related to how replicas switch from one ballot to another when computing the dependencies of a command. The problem may lead replicas to diverge and break the linearizability of the replicated service.

arXiv comments
Journal reference
DOI
Subjects
cs.DCDistributed, Parallel, and Cluster Computing

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Nov 2025 to Nov 2025.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Making Democracy Work: Fixing and Simplifying Egalitarian Paxos 1 comment

    • Thank you, dgacmu! We are currently working on a TLA+ specification with master's students, and we plan to verify it with TLC and Apalache. I discovered that Iulian's TLA+ specification was missing a ballot variable [1] by injecting a trace, because exhaustive exploration was…

      otrackView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.