Relational Verification of Distributed Systems via Weak Simulations

Abstract

Distributed systems are notoriously hard to get right, even when based on existing protocols. This thesis explores the use of executable specifications for (semi-) automatic verification of distributed systems. Rather than proving a distributed system is correct with respect to a given temporal property, this thesis proposes instead verifying a distributed system implements a given distributed protocol via per-node simulation. To prove a distributed system implements a protocol this thesis defines (1) contextual simulation logic, (2) simulation synthesis, and (3) fine-grained strategy improvement. Contextual simulation logic is a relational Hoare logic that consists of a judgement called contextual simulation and a set of inference rules to prove a contextual simulation valid. A contextual simulation relates an implementation program to a specification program via divergence preserving weak simulation. The set of rules are defined using the structure of both programs and used to align the implementation and specification programs. Simulation synthesis is a semi-algorithm that may prove or refute the validity of a (per-node) contextual simulation. Simulation synthesis is based on the game semantics of contextual simulation. Simulation synthesis will (1) construct a complete well-labeled simulation unwinding (a finite representation of a winning strategy proving the validity of a contextual simulation), (2) a counter-strategy to simulation of finite duration (a winning strategy refuting the validity of a contextual simulation), or (3) diverge. To solve a simulation game---an infinite state game of infinite duration---simulation synthesis incrementally expands and solves a finite-horizon of the game. Finite-horizon games are solved by reduction to satisfiability of quantified linear integer arithmetic (LIA) formulas. Further, this thesis develops fine-grained strategy improvement a decision procedure for proving (or refuting) satisfiability of quantified LIA formulas based on the game-semantics of LIA formulas. This procedure produces a certificate (a winning strategy proving or refuting) satisfiability of a LIA Formula. This certificate is used to construct the (winning) strategy for the finite-horizon game.