论文标题
将C11风格内存模型的Owicki-Gries集成到Isabelle/HOL中
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL
论文作者
论文摘要
弱记忆给程序验证带来了新的挑战，并导致了各种专业逻辑的发展。对于C11风格的内存模型，我们以前的工作表明，可以扩展Hoare逻辑和Owicki-Gries推理以验证弱内存程序的正确性。该技术在C11状态下引入了一组高级断言，以及一组基本的Hoare式公理，对原子弱记忆说明（例如，读取/写入），但保留了复合语句的所有其他标准证明义务。本文通过展示Nipkow和Nieto对Isabelle定理供体中Owicki-Gries的编码进行进一步进行这项工作，可以扩展以直接的方式处理C11风格的弱记忆模型。我们在文献中的几个石榴石测试和一个非平凡的例子中体现了我们的技术：彼得森适用于C11的算法。对于我们考虑的示例，可以使用Nipkow和Nieto开发的现有Isabelle策略自动放出证明大纲。这里的好处是，可以使用熟悉的伪代码语法编写程序，并直接嵌入到程序中。
Weak memory presents a new challenge for program verification and has resulted in the development of a variety of specialised logics. For C11-style memory models, our previous work has shown that it is possible to extend Hoare logic and Owicki-Gries reasoning to verify correctness of weak memory programs. The technique introduces a set of high-level assertions over C11 states together with a set of basic Hoare-style axioms over atomic weak memory statements (e.g., reads/writes), but retains all other standard proof obligations for compound statements. This paper takes this line of work further by showing Nipkow and Nieto's encoding of Owicki-Gries in the Isabelle theorem prover can be extended to handle C11-style weak memory models in a straightforward manner. We exemplify our techniques over several litmus tests from the literature and a non-trivial example: Peterson's algorithm adapted for C11. For the examples we consider, the proof outlines can be automatically discharged using the existing Isabelle tactics developed by Nipkow and Nieto. The benefit here is that programs can be written using a familiar pseudocode syntax with assertions embedded directly into the program.
