On Library Correctness under Weak Memory Consistency Specifying and Verifying Concurrent Libraries under Declarative Consistency Models
On Library Correctness under Weak Memory Consistency Specifying and Verifying Concurrent Libraries under Declarative Consistency Models
复制标题
DOI：
10.1145/3290381
复制
发表时间：
2019-01-01
影响因子：
1.8
通讯作者：
Vafeiadis, Viktor
中科院分区：
文献类型：
--
作者：
Raad, Azalea;Doko, Marko;Vafeiadis, Viktor
并发库是并发的基础。它们涵盖了以分层方式构建的一系列抽象（例如锁，交换器，堆栈，队列，套装）：更高级的库是由简单的库构建的。尽管在依次一致（SC）环境中验证此类库有很多工作，但对于如何在弱记忆一致性下指定和验证它们知之甚少（WMC）。我们提出了一个通用的声明框架并发图书馆声明，并根据其规格在构图上验证库实施。我们的框架足以编码标准模型，例如SC，（R）C11和TSO。此外，我们指定了几个并发库，包括相互排除锁，读取器锁，交换器，队列，堆栈和集合。然后，我们使用框架来验证锁，交换器，队列和堆栈的多个弱一致的实现。
Concurrent libraries are the building blocks for concurrency. They encompass a range of abstractions (e.g. locks, exchangers, stacks, queues, sets) built in a layered fashion: more advanced libraries are built out of simpler ones. While there has been a lot of work on verifying such libraries in a sequentially consistent (SC) environment, little is known about how to specify and verify them under weak memory consistency (WMC).We propose a general declarative framework that allows us to specify concurrent libraries declaratively, and to verify library implementations against their specifications compositionally. Our framework is sufficient to encode standard models such as SC, (R)C11 and TSO. Additionally, we specify several concurrent libraries, including mutual exclusion locks, reader-writer locks, exchangers, queues, stacks and sets. We then use our framework to verify multiple weakly consistent implementations of locks, exchangers, queues and stacks.