Library Abstraction for C / C + + Concurrency — extended version —
Library Abstraction for C / C + + Concurrency — extended version —
复制标题
C/C++ 并发的库抽象 — 扩展版本 —
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Mike Dodds
中科院分区：
文献类型：
--
作者：
Mark Batty;Mike Dodds
在构建复杂的并发系统时，抽象是至关重要的：程序员应该能够根据隐藏实现细节的抽象规范来推理并发库。宽松的内存模型在这方面提出了实质性的挑战，因为库不需要提供顺序一致的抽象：为了避免不必要的同步，它们可能允许客户端观察宽松的内存效应，库规范必须捕获这些。在本文中，我们提出了一个标准的声音库抽象在新的C11和C++11内存模型，推广标准的顺序一致的线性化概念。我们证明，我们的标准完全捕捉所有的客户端库的相互作用，通过调用和返回值，并通过微妙的同步效应所产生的内存模型。为了说明我们的方法，我们验证实现对规范的无锁Treiber堆栈和生产者消费者队列。我们的方法是第一个并发C11/C++11程序的组合推理方法。
When constructing complex concurrent systems, abstraction is vital: programmers should be able to reason about concurrent libraries in terms of abstract specifications that hide the implementation details. Relaxed memory models present substantial challenges in this respect, as libraries need not provide sequentially consistent abstractions: to avoid unnecessary synchronisation, they may allow clients to observe relaxed memory effects, and library specifications must capture these. In this paper, we propose a criterion for sound library abstraction in the new C11 and C++11 memory model, generalising the standard sequentially consistent notion of linearizability. We prove that our criterion soundly captures all client-library interactions, both through call and return values, and through the subtle synchronisation effects arising from the memory model. To illustrate our approach, we verify implementations against specifications for the lock-free Treiber stack and a producer-consumer queue. Ours is the first approach to compositional reasoning for concurrent C11/C++11 programs.
影响因子：
1.1
作者：
Filipovic I
通讯作者：
Filipovic I
所有权转移的线性化
影响因子：
0.6
作者：
Gotsman A
通讯作者：
Gotsman A
归咎于客户端：在存在指针的情况下对数据进行细化
影响因子：
1
作者：
Filipovic I
通讯作者：
Filipovic I