Verifying C11 programs operationally
Verifying C11 programs operationally
复制标题
DOI：
10.1145/3293883.3295702
复制
发表时间：
2018-11
期刊：
影响因子：
--
通讯作者：
Simon Doherty;Brijesh Dongol;H. Wehrheim;J. Derrick
中科院分区：
文献类型：
--
作者：
Simon Doherty;Brijesh Dongol;H. Wehrheim;J. Derrick
本文为C11存储器模型的发行片段开发了一种操作语义，并具有放松的访问。我们表明，相对于Batty等人的公理模型，语义既声音又完整。语义依赖于一个可观察性的每线程概念，该概念允许人们按程序顺序推理弱内存C11程序。最重要的是，我们为基于不变的推理开发了证据演算，我们用来验证Peterson的相互排除算法的发行版本。
This paper develops an operational semantics for a release-acquire fragment of the C11 memory model with relaxed accesses. We show that the semantics is both sound and complete with respect to the axiomatic model of Batty et al. The semantics relies on a per-thread notion of observability, which allows one to reason about a weak memory C11 program in program order. On top of this, we develop a proof calculus for invariant-based reasoning, which we use to verify the release-acquire version of Peterson's mutual exclusion algorithm.