将Owicki-Gries for C11-Style内存模型集成到Isabelle/HOL中
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL
摘要：
弱记忆对程序验证提出了新的挑战，并导致了各种专门逻辑的发展。对于C11类型的内存模型，我们以前的工作表明，它是可能的扩展霍尔逻辑和Owicki-Gries推理来验证弱内存程序的正确性。该技术在C11状态上引入了一组高级断言，以及一组原子弱内存语句上的基本霍尔式公理（例如，读/写），但保留所有其他标准的证明复合语句的义务。本文通过展示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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
