Open Collections

COMET : tractable reactive program synthesis

University of British Columbia

Reactive programs are programs that process external events, such as signals and messages. Device drivers and cloud microservices are examples of reactive programs. Systems built from reactive programs are concurrent and exhibit a high degree of nondeterminism, making non-exhaustive testing inadequate. A higher-level language can be used to write a specification: a formal definition of a program’s desired behaviour. Such specifications may be easier to reason about, but proofs of the specification say nothing of a low-level implementation. Program synthesis is one way to bridge this gap. A synthesizer searches a space of candidate programs for an implementation that satisfies the specification. In general, the number of candidate programs is infinite, making synthesis undecidable. Even a bounded search, e.g., on program length, soon becomes intractable as that search space grows exponentially. This work introduces COMET, a system for synthesizing reactive programs from unbounded nondeterministic iterative transformations (UNITY) specifications. Recent work in symbolic execution and solver-aided synthesis has advanced the state of the art, but symbolic techniques also lead to exponential blowup. COMET seeks to avoid exponential blowup by constraining the search space and synthesizing in small steps. COMET synthesizes non-trivial programs for sequential and concurrent languages by applying three techniques: symbolic execution of the specification into guarded traces, intermediate target trace synthesis, and recursive synthesis of target expressions. To evaluate this approach, I synthesize Arduino and Verilog programs from UNITY specifications of the Paxos consensus proposer and acceptor roles.

Text

2021-01-26

Attribution-ShareAlike 4.0 International

http://hdl.handle.net/2429/77177

Computer Science

University of British Columbia

UBCV

http://creativecommons.org/licenses/by-sa/4.0/