对具有松弛依赖关系的 C11 程序进行 Owicki-Gries 推理（扩展版）
计算机科学中的逻辑
2021-08-04 v1 编程语言
摘要
近年来，随着针对日益庞大的 C11 程序片段的操作语义及相关逻辑的发展，C11 程序的演绎验证技术取得了显著进步。然而，这些语义和逻辑是在一个受限的环境中开发的，以避免“读空气”问题。在本文中，我们提出了一种操作语义，该语义利用了由最近开发的基于指称事件结构的语义所导出的线程内偏序（称为语义依赖）。我们证明了我们的操作语义相对于该指称语义是可靠且完备的。我们提出了一个相关的逻辑，该逻辑推广了最近针对 RC11（修复后的 C11）的一个 Owicki-Gries 框架，并通过几个示例证明展示了该逻辑的用法。
引用
@article{arxiv.2108.01418,
title = {Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version)},
author = {Daniel Wright and Mark Batty and Brijesh Dongol},
journal= {arXiv preprint arXiv:2108.01418},
year = {2021}
}
备注
Extended version of the corresponding paper in FM2021