Efficient Synthesis of Symbolic Distributed Protocols by Sketching

TL;DR

This paper introduces Scythe, a novel synthesis tool for distributed protocols in TLA+ that combines sketching, syntax-guidance, and counterexample-guidance to efficiently generate large-scale protocols.

Contribution

It presents a new synthesis method that significantly reduces search space and is the first to support TLA+ for large-scale distributed protocol synthesis.

Findings

Successfully synthesized a Raft-based reconfiguration protocol at scale

Achieved orders of magnitude reduction in search space

Demonstrated effectiveness on diverse distributed protocol benchmarks

Abstract

We present a novel and efficient method for synthesis of parameterized distributed protocols by sketching. Our method is both syntax-guided and counterexample-guided, and utilizes a fast equivalence reduction technique that enables efficient completion of protocol sketches, often significantly reducing the search space of candidate completions by several orders of magnitude. To our knowledge, our tool, Scythe, is the first synthesis tool for the widely used specification language TLA+. We evaluate Scythe on a diverse benchmark of distributed protocols, demonstrating the ability to synthesize a large scale distributed Raft-based dynamic reconfiguration protocol beyond the scale of what existing synthesis techniques can handle.