Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification (Extended Version)

TL;DR

This paper introduces Cinnabar, a synthesis tool that helps designers model distributed agreement-based systems within a class that allows for efficient automated verification, addressing the challenge of opaque conditions for such classes.

Contribution

The paper presents Cinnabar, a synthesis-driven tool that guides system designers to model DAB systems within an efficiently-decidable class using counterexample-guided sketch completion.

Findings

Successfully synthesizes system completions for various DAB systems

Demonstrates efficiency in generating models fitting the decidable class

Addresses the opacity of conditions for efficient verification

Abstract

Distributed agreement-based (DAB) systems use common distributed agreement protocols such as leader election and consensus as building blocks for their target functionality. While automated verification for DAB systems is undecidable in general, recent work identifies a large class of DAB systems for which verification is efficiently-decidable. Unfortunately, the conditions characterizing such a class can be opaque and non-intuitive, and can pose a significant challenge to system designers trying to model their systems in this class. In this paper, we present a synthesis-driven tool, Cinnabar, to help system designers building DAB systems "fit" their intended designs into an efficiently-decidable class. In particular, starting from an initial sketch provided by the designer, Cinnabar generates sketch completions using a counterexample-guided procedure. The core technique relies on a compact encoding of a set of related counterexamples. We demonstrate Cinnabar's effectiveness by successfully and efficiently synthesizing completions for a variety of interesting DAB systems.