一句话：用 Coq 中 interaction trees 的单子解释为 LLVM IR 大型顺序子集建立模块化、可组合且可执行的形式语义。
本文为 LLVM IR 的一个大型顺序子集提出一种在 Coq 中机器化的新形式语义。与以往基于关系式操作语义的做法不同，该语义采用 interaction trees 的单子解释，从而在保持可提取可执行解释器的同时，获得更具组合性的语言语义定义方式。语义以事件处理器的方式模块化构造，能够处理 LLVM IR 的诸多非平凡语言特性，包括规约中的非确定性。作者扩展了 interaction trees 的弱互模拟等式理论以更好地处理非确定性，并据此得到组合式推理原则，进而证明所提取的参考解释器忠实精化语义模型。最后通过在单元测试及 HELIX 生成的 LLVM IR 程序上的评估验证了语义的正确性。
This paper presents a novel formal semantics, mechanized in Coq, for a large, sequential subset of the LLVM IR. In contrast to previous approaches, which use relationally-specified operational semantics, this new semantics is based on monadic interpretation of interaction trees, a structure that provides a more compositional approach to defining language semantics while retaining the ability to extract an executable interpreter. Our semantics handles many of the LLVM IR's non-trivial language features and is constructed modularly in terms of event handlers, including those that deal with nondeterminism in the specification. We show how this semantics admits compositional reasoning principles derived from the interaction trees equational theory of weak bisimulation, which we extend here to better deal with nondeterminism, and we use them to prove that the extracted reference interpreter faithfully refines the semantic model. We validate the correctness of the semantics by evaluating it on unit tests and LLVM IR programs generated by HELIX.
@article{paperbot1125,
title = {Modular, compositional, and executable formal semantics for LLVM IR},
author = {Yannick Zakowski and Calvin Beck and Irene Yoon and Ilia Zaichuk and Vadim Zaliva and Steve Zdancewic},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473572}
}