Porting operating systems is expensive; it costs time and money and (particularly) the attention of senior developers. Furthermore, with the end of Moore’s Law, portability is becoming more important again. Against this background, recent advances in program synthesis and the increasing availability of formal specifications for machine architectures offer an opportunity: it is now plausible to generate some or all of the code for an OS port rather than have to write it by hand.
I present Aquarium, an ecosystem of languages and tools I have designed and developed surrounding an assembly language synthesis engine. I have used Aquarium to produce code for a real (though small) operating system. Since the scalability of synthesis in general and assembly language synthesis in particular is limited, the core of this work is tooling for orchestrating the creation of small blocks of code to produce larger and useful procedures, a technique I call “compositional code generation”. I will also briefly discuss assembly synthesis itself and the assembly synthesis engines our group has developed.
David A. Holland just completed his Ph.D. at Harvard University, advised by Margo Seltzer and Stephen Chong. His dissertation covered leveraging program synthesis to port operating systems. His research interests are broad, ranging from formal verification to concurrent programming models to the use of nonvolatile memory in storage systems, and encompass prior work in operating systems, data provenance, and query languages for graph-structured data. He also wrote the OS/161 instructional operating system, and in his spare time is a NetBSD committer, where his primary focus is cleaning up code horrors that arise from non-local structural and design problems.
Galois is pleased to host this tech talk via live-stream for the public on January 22, 2021 from 1:00pm to 2:00pm Pacific Time. Send a request to email@example.com to receive meeting information.