Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL
复制标题
将 C11 型内存模型的 Owicki-Gries 集成到 Isabelle/HOL 中
DOI：
10.1007/s10817-021-09610-2
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Dalvandi S
中科院分区：
文献类型：
--
作者：
Dalvandi S
弱记忆对程序验证提出了新的挑战，并导致了各种专门逻辑的发展。对于C11风格的内存模型，我们以前的工作表明，它是可能的扩展Hoare逻辑和Owicki-Gries推理，以验证弱内存程序的正确性。该技术在C11状态上引入了一组高级断言，以及一组原子弱内存语句（例如读/写）上的基本霍尔式公理，但保留了复合语句的所有其他标准证明义务。本文采取这条线的工作进一步介绍了第一个演绎验证环境中的Isabelle/HOL C11类弱内存程序。这个验证环境是建立在Nipkow和Nieto的Owicki-Gries在Isabelle定理证明器中的编码上的。我们将我们的技术从文献和两个非平凡的例子：彼得森的算法和适用于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 introducing the first deductive verification environment in Isabelle/HOL for C11-like weak memory programs. This verification environment is built on the Nipkow and Nieto’s encoding of Owicki–Gries in the Isabelle theorem prover. We exemplify our techniques over several litmus tests from the literature and two non-trivial examples: Peterson’s algorithm and a read–copy–update 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.
登录
查看更多内容
DOI：
10.1145/3293883.3295702
发表时间：
2018-11
期刊：
Proceedings of the 24th Symposium on Principles and Practice of Parallel Programming
影响因子：
--
作者：
Simon Doherty;Brijesh Dongol;H. Wehrheim;J. Derrick
通讯作者：
Simon Doherty;Brijesh Dongol;H. Wehrheim;J. Derrick
影响因子：
1.8
作者：
Kokologiannakis, Michalis;Lahav, Ori;Vafeiadis, Viktor
通讯作者：
Vafeiadis, Viktor
DOI：
10.1007/978-3-642-37036-6_28
发表时间：
2012-07
期刊：
--
影响因子：
--
作者：
J. Alglave;D. Kroening;Vincent Nimal;Michael Tautschnig
通讯作者：
J. Alglave;D. Kroening;Vincent Nimal;Michael Tautschnig
DOI：
10.1007/bfb0030541
发表时间：
1994
期刊：
--
影响因子：
--
作者：
Lawrence Charles Paulson
通讯作者：
Lawrence Charles Paulson
使用 Event-B 和 ProB 进行 C11 程序的演绎验证
DOI：
10.1145/3340672.3341117
发表时间：
2019
期刊：
--
影响因子：
--
作者：
Dalvandi M
通讯作者：
Dalvandi M