VerC3: A Library for Explicit State Synthesis of Concurrent Systems
Marco Elvera, Christopher J. Banksb, Paul Jacksonc and Vijay Nagarajand
University of Edinburgh
amarco.elver@ed.ac.uk
bc.banks@ed.ac.uk
cpaul.jackson@ed.ac.uk
dvijay.nagarajan@ed.ac.uk
ABSTRACT
We propose an alternative, explicit state only, approach to concurrent system synthesis. In particular, the focus of this work is on the synthesis of distributed protocols. Given a correctness specification and a protocol skeleton (i.e. incomplete with holes), the goal is to synthesize the holes. At the heart of our technique is a dynamic programming based algorithm that prunes inferred failure candidates. The algorithm exploits the fact that typically only a few transitions are needed to reach an erroneous state in a faulty distributed protocol. Therefore, it is unlikely that every hole to be synthesized is contributing towards the error; thus, faulty protocol candidates where only a subset of holes were used can be used to infer failures of later candidates with a superset of holes. We evaluate the tool using a cache coherence protocol synthesis case study. Specifically, we study a directory based MSI protocol, assuming an unordered interconnect which gives rise to numerous race conditions which must be resolved via introducing transient states–a common cause of complexity and bugs in such protocols. In the case study, we therefore focus on synthesizing the transient state actions (we consider up to 12 holes out of possible 35). With the proposed candidate pruning optimization, we report up to 43x improvement over a naïve candidate enumeration scheme. We make available the tool and C++ library, VerC3.
