将用于 C11 风格内存模型的 Owicki-Gries 推理集成到 Isabelle/HOL 中
编程语言
2020-04-10 v2 计算机科学中的逻辑
摘要
弱内存为程序验证带来了新挑战，并促使了多种专用逻辑的发展。对于 C11 风格内存模型，我们此前的工作已表明可扩展 Hoare 逻辑与 Owicki-Gries 推理来验证弱内存程序的正确性。该技术引入了一组关于 C11 状态的高层断言以及一组关于原子弱内存语句（如读/写）的基本 Hoare 风格公理，但保留了用于复合语句的所有其他标准证明义务。本文推进了这一工作线，表明 Nipkow 与 Nieto 在 Isabelle 定理证明器中对 Owicki-Gries 的编码可以直接扩展以处理 C11 风格弱内存模型。我们借助文献中的若干 litmus 测试以及一个非平凡例子——适用于 C11 的 Peterson 算法——来示例我们的技术。对于我们考虑的例子，证明概要可使用 Nipkow 与 Nieto 开发的现有 Isabelle 策略自动解除。其益处在于程序可使用熟悉的伪代码语法编写，并将断言直接嵌入程序中。
引用
@article{arxiv.2004.02983,
title = {Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL},
author = {Sadegh Dalvandi and Brijesh Dongol and Simon Doherty},
journal= {arXiv preprint arXiv:2004.02983},
year = {2020}
}