一句话：用两个 DSL 与符号执行合成引擎自动生成操作系统的机器相关汇编代码，实现 OS 移植。
摩尔定律终结带来硬件多样化，操作系统可移植性愈发关键。本文探索用现代程序合成自动生成操作系统的机器相关部分。作者设计了两个 DSL：Alewife 用于以机器无关方式描述机器相关的 OS 功能，Cassiopea 用于描述指令集架构语义。工具链根据 Alewife 规约与 Cassiopea 机器描述，将机器无关规约特化到目标 ISA，并借助定制的符号执行引擎合成汇编实现；同时提出若干面向 OS 汇编合成的优化以提升可扩展性。评估中从两个已有 OS 出发，为四个真实硬件平台成功合成 140 个 OS 组件，证明了该方法的可行性，并讨论了其优势与尚存的研究挑战。
The end of Moore’s Law has ushered in a diversity of hardware not seen in decades. Operating system (OS) (and system software) portability is accordingly becoming increasingly critical. Simultaneously, there has been tremendous progress in program synthesis. We set out to explore the feasibility of using modern program synthesis to generate the machine-dependent parts of an operating system. Our ultimate goal is to generate new ports automatically from descriptions of new machines. One of the issues involved is writing specifications, both for machine-dependent operating system functionality and for instruction set architectures. We designed two domain-specific languages: Alewife for machine-independent specifications of machine-dependent operating system functionality and Cassiopea for describing instruction set architecture semantics. Automated porting also requires an implementation. We developed a toolchain that, given an Alewife specification and a Cassiopea machine description, specializes the machine-independent specification to the target instruction set architecture and synthesizes an implementation in assembly language with a customized symbolic execution engine. Using this approach, we demonstrate the successful synthesis of a total of 140 OS components from two pre-existing OSes for four real hardware platforms. We also developed several optimization methods for OS-related assembly synthesis to improve scalability. The effectiveness of our languages and ability to synthesize code for all 140 specifications is evidence of the feasibility of program synthesis for machine-dependent OS code. However, many research challenges remain; we also discuss the benefits and limitations of our synthesis-based approach to automated OS porting.
@article{paperbot2139,
title = {Towards Porting Operating Systems with Program Synthesis},
author = {Jingmei Hu and Eric Lu and David A. Holland and Ming Kawaguchi and Stephen Chong and Margo Seltzer},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {45},
number = {1},
year = {2023},
doi = {10.1145/3563943}
}