We introduce a new algorithm for an unbounded concurrent double-ended queue (deque). Like the bounded deque of Herlihy, Luchangco, and Moir on which it is based, the new algorithm is simple and obstruction free, has n...
详细信息
ISBN:
(纸本)9781509028238
We introduce a new algorithm for an unbounded concurrent double-ended queue (deque). Like the bounded deque of Herlihy, Luchangco, and Moir on which it is based, the new algorithm is simple and obstruction free, has no pathological long-latency scenarios, avoids interference between operations at opposite ends, and requires no special hardware support beyond the usual compare-and-swap. To the best of our knowledge, no prior concurrent deque combines these properties with unbounded capacity, or provides consistently better performance across a wide range of concurrent workloads.
A dual container has the property that when it is empty, the remove method will insert an explicit reservation ("antidata") into the container, rather than returning an error flag. This convention gives the ...
详细信息
ISBN:
(纸本)9781450329446
A dual container has the property that when it is empty, the remove method will insert an explicit reservation ("antidata") into the container, rather than returning an error flag. This convention gives the container explicit control over the order in which pending requests will be satisfied once data becomes available. The dual pattern also allows the method's caller to spin on a thread-local flag, avoiding memory contention. In this paper we introduce a new nonblocking construction that allows any nonblocking container for data to be paired with almost any nonblocking container for antidata. This construction provides a composite ordering discipline-e.g., it can satisfy pending pops from a stack in FIFO order, or satisfy pending dequeues in order of thread priority.
Modern computer systems often involve multiple processes or threads of control that communicatethrough shared memory. However, the implementation of correct and efficient datastructures that can be shared by several p...
详细信息
Modern computer systems often involve multiple processes or threads of control that communicatethrough shared memory. However, the implementation of correct and efficient datastructures that can be shared by several processes is frequently challenging. This thesis is concerned with the design and verification of a class of shared memory algorithms known as nonblocking algorithms, which are implementations of shared data structures that provide strong progress guarantees. nonblocking algorithms offer an appealing alternative to traditional techniques for the implementation of shared memory data structures, but they are difficult to design, and extant algorithms can often be applied in only a limited range of systems. Furthermore, because of their subtlety, it is notoriously difficult to determine whether a given nonblocking algorithm is correct. This thesis addresses these difficulties in two ways. First, we present techniques for theverification of nonblocking algorithms that dynamically allocate memory. These techniquesallow the construction of formal and complete proofs of correctness, so that each proof maybe checked by a mechanical proof assistant. Applying techniques first developed for theverification of distributed algorithms, we use labelled-transition systems to model algorithmsand their specifications, and simulation relations to prove that an implementation meets itsspecification. nonblocking algorithms often require a particular notion of simulation, calledbackward simulation, that is rarely necessary in other contexts. This thesis contributes to therelatively limited collective experience in the use of backward simulation. The second set of contributions addresses the limitations of many extant nonblocking algorithms. While many nonblocking algorithms allocate memory dynamically, it is difficult to determine in a nonblocking context when it is safe to free memory. We present techniques to accomplish this. Furthermore, many nonblocking algorithms depend
Efficient communication and synchronization is crucial for fine-grained parallelism. Libraries providing such features, while indispensable, are difficult to write, and often cannot be tailored or composed to meet the...
详细信息
ISBN:
(纸本)9781450312059
Efficient communication and synchronization is crucial for fine-grained parallelism. Libraries providing such features, while indispensable, are difficult to write, and often cannot be tailored or composed to meet the needs of specific users. We introduce reagents, a set of combinators for concisely expressing concurrency algorithms. Reagents scale as well as their hand-coded counterparts, while providing the composability existing libraries lack.
暂无评论