Hardware communication and coordination protocols are the backbone of today’s highly integrated Systems-on-Chip (SoC) designs, which are ubiquitous in mobile and embedded computing platforms. Even when employing the state of-the-art design practices, designers are still called upon to create the entire design, including the most mundane but error-prone low-level aspects of the design, which arguably leads to tedious design and presence of bugs. The goal of this theme is to explore how synthesis can simplify and improve the design process for multicore protocols.
We have proposed a new way to program distributed protocols using concolic snippets, which are sample execution fragments that contain both concrete and symbolic values. This approach allows the programmer to describe the desired system partially using the traditional model of communicating extended finite-state- machines (EFSMs) along with high-level invariants and concrete execution fragments. Our tool derives a protocol implementation from a set of EFSM skeletons, which is analyzed using a model-checker with respect to the desired invariants. The programmer can add new concrete execution fragments to fix the counter-examples produced by the model-checker. In [URDMA13] we show that (1) for a classical cache coherence protocol, our tool automatically generates a complete implementation from an EFSM skeleton and a few concrete examples for every transition, and (2) a published partial description of the SGI-Origin coherence protocol maps directly into symbolic examples and leads to a complete implementation in a few model-checker iterations. This effort was inspired by the program synthesis tool Sketch and the work on programming by examples, and integrates a diverse range of ideas from ExCAPE team members.
Scenarios, or Message Sequence Charts, offer an intuitive way of describing the desired behaviors of a distributed protocol. Recently, we have proposed a new way of specifying finite-state protocols using scenarios: we show that it is possible to automatically derive a distributed implementation from a set of scenarios, augmented with a set of safety and liveness requirements, provided the given scenarios adequately “cover” all the states of the desired implementation. We first derive incomplete state machines from the given scenarios, and then synthesis corresponds to completing the transition relation of individual processes so that the global product meets the specified requirements. This completion problem, in general, has the same complexity, PSPACE, as the verification problem, but unlike the verification problem, is NP-complete for a constant number of processes. We have developed two algorithms for solving the completion problem, one based on a heuristic search in the space of possible completions, and one based on a symbolic encoding using OBDDs. We have shown how classical distributed protocols such as the alternating-bit protocol, can be specified in more intuitive ways using this approach [AMRSTU14].
This work integrates multiple research themes within ExCAPE: the design methodology allows the user to mix different styles of specifications (scenarios, protocol skeletons, and correctness requirements), and is inspired by the work on program sketching; and the computational back-end uses ideas from counter-example guided inductive synthesis. Future work in this project will focus on deriving communicating Extended Finite-State Machines. This will allow the tool to handle more general protocols, and in particular, we plan to focus on industrial-strength protocols for memory consistency and coherence. To solve the computational synthesis problem in this more general setting, we plan to use the emerging infrastructure for the SyGuS (Syntax-Guided Synthesis) problem.
We have been working on the efficient synthesis of control logic for failure avoidance in multi-threaded programs, specifically on: (i) a new synthesis technique for deadlock avoidance that employs SAT solvers coupled with controltheoretic methods for systems modeled with Petri nets; and (ii) a new approach for tackling classes of atomicity violations by developing synthesis techniques for Petri nets subject to regular language specifications [BWL14]. The goal in (i) is to achieve greater scalability than prior approaches developed by PI Lafortune and his co-workers in the context of the Gadara project, by exploiting the power of SAT solvers. The goal in (ii) is to synthesize state-partition-based supervisors for enforcing regular language specifications. This will provide the necessary theoretical foundations for tackling atomicity violations in multi-threaded programs by supervisory control techniques.
This project rethinks how to construct compilers. Specifically, we ask whether a compiler based on a sequence of synthesis problems can avoid the need for the classical analyses and transformations, which make compilers laborious to develop. In this project, we developed Chlorophyll, a synthesis-aided programming model and compiler for GreenArrays 144, an extremely minimalist low-power spatial architecture that requires partitioning the program into fragments of no more than 256 instructions and 64 words of data. This processor is 100x more energy efficient than its competitors, but it can currently be programmed only by using a low-level stack-based language. Chlorophyll allows programmers to provide human insight by specifying partial partitioning of data and computation. The compiler relies on synthesis, sidestepping the need to develop classical optimizations, which may be challenging given the unusual architecture. To scale synthesis to real problems, we decompose it into smaller synthesis subproblema-partitioning, layout, and code generation. We show that the synthesized programs are no more than 30% slower than highly optimized expert-written programs and faster than programs produced by a heuristic, non-synthesizing version of our compiler [PJSTCB14]. The students on this project won the Qualcomm Innovation Fellowship.
- R. Alur, M. Martin, M. Raghothaman, C. Stergiou, S. Tripakis, and A. Udupa. Synthesizing finite-state protocols from scenarios and requirements. 10th Haifa Verification Conference, 2014.
- A. Butez, Y.Wang, and S. Lafortune. State-partition-based control of discrete event systems for enforcement of regular language specifications. In IFAC World Congress 2014.
- P M. Phothilimthana, T. Jelves, R. Shah, N. Totla, S. Chasins, and R. Bodík. Chlorophyll: Synthesis-aided compiler for lowpower spatial architectures. In ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2014.
- A. Udupa, A. Raghavan, J. V. Deshmukh, S. Mador-Haim, M. M. K. Martin, R. Alur. TRANSIT: specifying protocols with concolic snippets. PLDI 2013: 287-296