小步长 Cminor 的分离逻辑

Cminor 是一种中级命令式编程语言；存在从 C 到 Cminor 以及从 Cminor 到机器语言的已证明正确的优化编译器。我们重新设计了 Cminor 使其适用于 Hoare Logic 推理，并为 Cminor 设计了分离逻辑。在本文中，我们给出了一种小步长语义（而非已证明正确编译器所采用的大步长语义），这是由支持未来并发扩展的需求所驱动的。我们详细阐述了关于分离逻辑可靠性的机器验证证明。这是首次针对小步长语义的大规模分离逻辑机器验证证明。本文所述工作是在 Coq 证明助手中完成的。它是迈向这样一个环境的第一步：在该环境中，可以使用分离逻辑验证并发 Cminor 程序，并通过具有形式化端到端正确性保证的已证明正确编译器进行编译。