A declarative approach to specifying Paxos using three-valued modal fixpoint logic

Abstract

We present Three-valued Fixpoint Quorum Logic, or 3muQL for short; a three-valued modal fixed-point logic designed for declaratively specifying and reasoning about distributed algorithms, such as the Paxos consensus algorithm. Our methodology represents a distributed algorithm as a logical theory, enabling correctness properties to be derived directly within the framework -- or revealing logical errors in the algorithm's design when they exist. 3muQL adopts a declarative approach, specifying the overall logic of computation without prescribing control flow. Notably, message-passing and state-transitions are not explicitly modelled, and notions of 'quorum' are abstracted from concrete thresholds to abstract modal operators. This distinguishes our framework from approaches like TLA+. The logical abstraction emphasises the essence of distributed algorithms, offering a novel perspective on their specification and reasoning. We define the syntax and semantics of 3muQL, explore its theoretical properties, and demonstrate its applicability through a detailed treatment of the Paxos consensus algorithm. By presenting Paxos as a logical theory and deriving its standard correctness properties, we showcase the framework's capacity to handle non-trivial distributed systems. We envision 3muQL as a versatile tool for specifying and reasoning about distributed algorithms. The Paxos example highlights the framework's ability to capture intricate details, offering a new lens through which distributed algorithms can be specified, studied, and checked. The ideas we present are easily implemented, and to demonstrate this we have implemented a freely-available proof-of- concept 3muQL model-checker, as an effective prototyping tool.