Toward Automatic Operating System Ports via Code Generation and Synthesis
Author
Holland, David Andrew
Metadata
Show full item recordCitation
Holland, David Andrew. 2020. Toward Automatic Operating System Ports via Code Generation and Synthesis. Doctoral dissertation, Harvard University, Graduate School of Arts & Sciences.Abstract
Porting operating systems is expensive. Recent developments in formal specifications of machine architectures and in program synthesis have made it possible to consider generating code for operating system ports rather than needing to write it by hand. Several challenges arise, the foremost being the current scaling limits of program synthesis for assembly language.In this dissertation I take a system-level approach to generating ports of a small operating system. I present Aquarium, an ecosystem of languages and tools I designed to surround an assembly language synthesis engine. Chief among these are Grayling, a special-purpose compiler for context switch code, and Grouper, a tool implementing an approach I call compositional code generation, generating code in units of small synthesizable blocks. I have deployed these tools in the context of a simple though realistic operating system called Goldfish, and successfully generated working code for a number of machine-dependent operating system components.
Terms of Use
This article is made available under the terms and conditions applicable to Other Posted Material, as set forth at http://nrs.harvard.edu/urn-3:HUL.InstRepos:dash.current.terms-of-use#LAACitable link to this page
https://nrs.harvard.edu/URN-3:HUL.INSTREPOS:37365798
Collections
- FAS Theses and Dissertations [5439]
Contact administrator regarding this item (to report mistakes or request changes)