VerC3: A Library for Explicit State Synthesis of Concurrent Systems

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationDesign, Automation, and Test in Europe, Topic E2: Compilers and Software Synthesis
Place of PublicationDresden, Germany
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages1375-1380
Number of pages6
ISBN (Electronic)978-3-9819263-0-9
DOIs
Publication statusPublished - 23 Apr 2018
Event21st Design, Automation and Test in Europe - Dresden, Germany
Duration: 19 Mar 201823 Mar 2018
https://www.date-conference.com/

Publication series

Name
PublisherIEEE
ISSN (Electronic)1558-1101

Conference

Conference21st Design, Automation and Test in Europe
Abbreviated titleDATE 2018
Country/TerritoryGermany
CityDresden
Period19/03/1823/03/18
Internet address

Fingerprint

Dive into the research topics of 'VerC3: A Library for Explicit State Synthesis of Concurrent Systems'. Together they form a unique fingerprint.

Cite this