Library abstraction for C/C++ concurrency
Library abstraction for C/C++ concurrency
复制标题
C/C 并发的库抽象
DOI：
10.1145/2429069.2429099
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Batty M
中科院分区：
文献类型：
--
作者：
Batty M
在构建复杂的并发系统时，抽象是至关重要的：程序员应该能够根据隐藏实现细节的抽象规范来推断并发库。放松内存模型在这方面提出了实质性的挑战，因为库不需要提供顺序一致的抽象：为了避免不必要的同步，它们可能允许客户端观察放松内存效果，而库规范必须捕获这些。在本文中，我们提出了在新的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.
登录
查看更多内容
责备客户：关于指针存在下的数据细化
DOI：
--
发表时间：
2010
期刊：
影响因子：
--
作者：
Hongseok Yang
通讯作者：
Hongseok Yang
C/C++ 并发的库抽象 — 扩展版本 —
DOI：
--
发表时间：
2012
期刊：
影响因子：
--
作者：
Mark Batty;Mike Dodds
通讯作者：
Mike Dodds
所有权转移的线性化
影响因子：
0.6
作者：
Gotsman A
通讯作者：
Gotsman A
影响因子：
1.1
作者：
Filipovic I
通讯作者：
Filipovic I
了解 POWER 多处理器
影响因子：
--
作者：
Sarkar S
通讯作者：
Sarkar S