Shellac: A Compiler Synthesizer for Concurrent Programs

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 compiler synthesizer that completes a sketch of a syntax-directed compiler by using program synthesis to derive translation rules. This approach produces a correct-by-construction compiler without burdening the compiler writer with manual specification and verification. We evaluate Shellac by synthesizing a compiler from unity to Arduino C++ and Verilog, then compiling Paxos consensus in unity to implementations in Arduino C++ for microcontrollers and Verilog for reconfigurable hardware.