Compiler Synthesis


Shellac synthesizes compiler rules from specification to implementation languages.

Formal specification languages such as TLA+ and unity are used to design and verify concurrent programs. These languages are intended for analysis rather than for execution. A compiler or a human must implement the specified program in a lower-level executable language. We present Shellac, a synthesized compiler from unity to Arduino C++ and Verilog. The approach is essentially syntax-directed translation, where the translation rules are automatically generated via program synthesis. This approach produces a correct-by-construction compiler without burdening the compiler writer with manual specification and verification. We evaluate Shellac by compiling Paxos consensus in unity to implementations in Arduino C++ for microcontrollers and Verilog for reconfigurable hardware.

Additional Information

Venue: Presented at VSTTE 2022: 14th International Conference on Verified Software: Theories, Tools, and Experiments


Artifacts: Source code and PDF is available.

People: Christopher Chen, Mark Greenstreet, Margo Selzer

arrow_back Back

Systopia lab is supported by a number of government and industrial sources, including Cisco Systems, the Communications Security Establishment Canada, Intel Research, the National Sciences and Engineering Research Council of Canada (NSERC), Network Appliance, Office of the Privacy Commissioner of Canada, and the National Science Foundation (NSF).