Automatic Completion of Distributed Protocols with Symmetry

TL;DR

This paper presents a counterexample-guided synthesis method for automatically completing distributed protocols with symmetry constraints, simplifying the design of correct protocols by filling in unknown functions.

Contribution

It introduces a novel synthesis algorithm combining SMT-based candidate generation with symmetry-aware constraints and model checking for correctness verification.

Findings

Successfully completed protocols for mutual exclusion, self-stabilization, and cache coherence.

Demonstrated the effectiveness of the approach in automatically discovering missing protocol details.

Validated the method's ability to handle safety, liveness, and fairness requirements in distributed protocols.

Abstract

A distributed protocol is typically modeled as a set of communicating processes, where each process is described as an extended state machine along with fairness assumptions, and its correctness is specified using safety and liveness requirements. Designing correct distributed protocols is a challenging task. Aimed at simplifying this task, we allow the designer to leave some of the guards and updates to state variables in the description of extended state machines as unknown functions. The protocol completion problem then is to find interpretations for these unknown functions while guaranteeing correctness. In many distributed protocols, process behaviors are naturally symmetric, and thus, synthesized expressions are further required to obey symmetry constraints. Our counterexample-guided synthesis algorithm consists of repeatedly invoking two phases. In the first phase, candidates for unknown expressions are generated using the SMT solver Z3. This phase requires carefully orchestrating constraints to enforce the desired symmetry in read/write accesses. In the second phase, the resulting completed protocol is checked for correctness using a custom-built model checker that handles fairness assumptions, safety and liveness requirements, and exploits symmetry. When model checking fails, our tool examines a set of counterexamples to safety/liveness properties to generate constraints on unknown functions that must be satisfied by subsequent completions. For evaluation, we show that our prototype is able to automatically discover interesting missing details in distributed protocols for mutual exclusion, self stabilization, and cache coherence.