Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient Synthesis of Symbolic Distributed Protocols by Sketching

Derek Egolf, William Schultz, Stavros Tripakis

TL;DR

This work tackles the automated synthesis of parameterized distributed protocols by introducing a true syntax-guided, counterexample-guided synthesis framework for TLA+-specifiable systems. The core method, implemented in the Scythe tool, combines cache-based expression generation with equivalence reduction and a pruning-constraint mechanism driven by counterexamples, enabling scalable completion of protocol sketches. It demonstrates the ability to synthesize nontrivial, infinite-state protocols, including Raft-based dynamic reconfiguration, and provides formal correctness guarantees for all instances via TLAPS proofs in many cases. The approach offers a practical path to designing correct distributed protocols at scale, reducing search complexity dramatically and enabling verification-supported synthesis for real-world specifications.

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.

Efficient Synthesis of Symbolic Distributed Protocols by Sketching

TL;DR

This work tackles the automated synthesis of parameterized distributed protocols by introducing a true syntax-guided, counterexample-guided synthesis framework for TLA+-specifiable systems. The core method, implemented in the Scythe tool, combines cache-based expression generation with equivalence reduction and a pruning-constraint mechanism driven by counterexamples, enabling scalable completion of protocol sketches. It demonstrates the ability to synthesize nontrivial, infinite-state protocols, including Raft-based dynamic reconfiguration, and provides formal correctness guarantees for all instances via TLAPS proofs in many cases. The approach offers a practical path to designing correct distributed protocols at scale, reducing search complexity dramatically and enabling verification-supported synthesis for real-world specifications.

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.
Paper Structure (26 sections, 5 theorems, 3 equations, 1 figure, 1 table)

This paper contains 26 sections, 5 theorems, 3 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Protocol Representation in TLA+
  4. Protocol Semantics
  5. Properties and Verification
  6. Modeling Conventions
  7. Synthesis of Distributed Protocols
  8. Protocol Sketches
  9. Problem Statements
  10. Our Approach
  11. Expression Generation
  12. Naive Breadth-First Algorithm
  13. Cache-Based Algorithm
  14. Equivalence Reduction
  15. Counterexamples and Pruning Constraints
  16. ...and 11 more sections

Key Result

Theorem 1

Let $r$ be a counterexample of a completion of the sketch $S$. If $r$ is a safety violation then $\pi_\textit{safe}(r\xspace)$ is optimal w.r.t. $r$ and $S$. If $r$ is a deadlock, liveness, or stuttering violation then $\pi_\textit{dead}(r\xspace)$, $\pi_\textit{live}(r\xspace)$, and $\pi_\textit{st

Figures (1)

  • Figure 1: An example of a TLA+ protocol (excerpt).

Theorems & Definitions (9)

  • Theorem 1
  • Theorem 2
  • proof
  • Theorem 3
  • proof
  • Theorem 4
  • proof
  • Theorem 5
  • proof