A case study on parametric verification of failure detectors

Partial synchrony is a model of computation in many distributed algorithmsand modern blockchains. These algorithms are typically parameterized in thenumber of participants, and their correctness requires the existence of boundson message delays and on the relative speed of processes after reaching GlobalStabilization Time. These characteristics make partially synchronous algorithmsparameterized in the number of processes, and parametric in time bounds, whichrender automated verification of partially synchronous algorithms challenging.In this paper, we present a case study on formal verification of both safetyand liveness of the Chandra and Toueg failure detector that is based on partialsynchrony. To this end, we first introduce and formalize the class of symmetricpoint-to-point algorithms that contains the failure detector. Second, we showthat these symmetric point-to-point algorithms have a cutoff, and the cutoffresults hold in three models of computation: synchrony, asynchrony, and partialsynchrony. As a result, one can verify them by model checking small instances,but the verification problem stays parametric in time. Next, we specify thefailure detector and the partial synchrony assumptions in three frameworks:TLA+, IVy, and counter automata. Importantly, we tune our modeling to use thestrength of each method: (1) We are using counters to encode message bufferswith counter automata, (2) we are using first-order relations to encode messagebuffers in IVy, and (3) we are using both approaches in TLA+. By running thetools for TLA+ and counter automata, we demonstrate safety for fixed timebounds. By running IVy, we prove safety for arbitrary time bounds. Moreover, weshow how to verify liveness of the failure detector by reducing theverification problem to safety verification. Thus, both properties are verifiedby developing inductive invariants with IVy