论文标题
验证C11风格的弱内存库
Verifying C11-Style Weak Memory Libraries
论文作者
论文摘要
到目前为止，在弱记忆下对并发程序的演绎验证仅限于整体状态空间上的简单程序。为了缩小性，我们还需要具有可验证库抽象的模块化技术。本文在RC11 RAR的背景下解决了这一挑战，RC11 RAR是C11存储器模型的子集，该模型接纳了放松和发行的通道访问权限，但可以放弃所谓的，即负载缓冲的周期。我们开发了一个简单的框架，用于指定抽象对象，以精确表征抽象方法调用的可观察性保证。我们展示了如何将该框架与操作语义集成，该语义可以验证客户程序中执行抽象方法调用的客户端程序。最后，我们展示了如何通过为抽象对象开发（上下文）完善框架来验证RC11 RAR中此类抽象的实现。我们的框架，包括操作语义，客户图书馆程序的验证技术以及抽象库及其实现之间的模拟，在Isabelle/Hol中进行了机械化。
Deductive verification of concurrent programs under weak memory has thus far been limited to simple programs over a monolithic state space. For scalabiility, we also require modular techniques with verifiable library abstractions. This paper addresses this challenge in the context of RC11 RAR, a subset of the C11 memory model that admits relaxed and release-acquire accesses, but disallows, so called, load-buffering cycles. We develop a simple framework for specifying abstract objects that precisely characterises the observability guarantees of abstract method calls. We show how this framework can be integrated with an operational semantics that enables verification of client programs that execute abstract method calls from a library it uses. Finally, we show how implementations of such abstractions in RC11 RAR can be verified by developing a (contextual) refinement framework for abstract objects. Our framework, including the operational semantics, verification technique for client-library programs, and simulation between abstract libraries and their implementations, has been mechanised in Isabelle/HOL.
