Verifying Concurrent Data Structures by Simulation

We describe an approach to verifying concurrent data structures based on simulation between two Input/Output Automata (IOAs), modelling the specification and the implementation. We explain how we used this approach in mechanically verifying a simple lock-free stack implementation using forward simulation, and briefly discuss our experience in verifying three other lock-free algorithms which all required the use of backward simulation.     

Software transactional memory

Summary.  As we learn from the literature, flexibility in choosing synchronization operations greatly simplifies the task of designing highly concurrent programs. Unfortunately, existing hardware is inflexible and is at best on the level of a Load–Linked/Store–Conditional operation on a single word. Building on the hardware based transactional synchronization methodology of Herlihy and Moss, we offer software transactional memory (STM), a novel software method for supporting flexible transactional programming of synchronization operations. STM is non-blocking, and can be implemented on existing machines using only a Load–Linked/Store–Conditional operation. We use STM to provide a general highly concurrent method for translating sequential object implementations to non-blocking ones based on implementing a k-word compare&swap STM-transaction. Empirical evidence collected on simulated multiprocessor architectures shows that our method always outperforms the non-blocking translation methods in the style of Barnes, and outperforms Herlihy’s translation method for sufficiently large numbers of processors. The key to the efficiency of our software-transactional approach is that unlike Barnes style methods, it is not based on a costly “recursive helping” policy. Received: January 1996 / Revised: June 1996 / Accepted: August 1996     

Lock-free parallel dynamic programming

We show a method for parallelizing top down dynamic programs in a straightforward way by a careful choice of a lock-free shared hash table implementation and randomization of the order in which the dynamic program computes its subproblems. This generic approach is applied to dynamic programs for knapsack, shortest paths, and RNA structure alignment, as well as to a state-of-the-art solution for minimizing the maximum number of open stacks. Experimental results are provided on three different modern multicore architectures which show that this parallelization is effective and reasonably scalable. In particular, we obtain over 10 times speedup for 32 threads on the open stacks problem.     

An optimistic approach to lock-free FIFO queues

First-in-first-out (FIFO) queues are among the most fundamental and highly studied concurrent data structures. The most effective and practical dynamic-memory concurrent queue implementation in the literature is the lock-free FIFO queue algorithm of Michael and Scott, included in the standard Java ^TM Concurrency Package. This work presents a new dynamic-memory concurrent lock-free FIFO queue algorithm that in a variety of circumstances performs better than the Michael and Scott queue. The key idea behind our new algorithm is a novel way of replacing the singly-linked list of Michael and Scott, whose pointers are inserted using a costly compare-and-swap (CAS) operation, by an “optimistic” doubly - linked list whose pointers are updated using a simple store, yet can be “fixed” if a bad ordering of events causes them to be inconsistent. We believe it is the first example of such an “optimistic” approach being applied to a real world data structure. A preliminary version of this paper appeared in the proceedings of the 18th International Conference on Distributed Computing (DISC) 2004, pages 117–131.     

Laziness pays! Using lazy synchronization mechanisms to improve non-blocking constructions

Summary. We present a simple and efficient wait-free implementation of Lazy Large Load-Linked/Store-Conditional (Lazy-LL/SC), which can be used to atomically modify a dynamically-determined set of shared variables in a lock-free manner. The semantics of Lazy-LL/SC is weaker than that of similar objects used by us previously to design lock-free and wait-free constructions, and as a result can be implemented more efficiently. However, we show that Lazy-LL/SC is strong enough to be used in existing non-blocking universal constructions and to build new ones. Received: December 2000 / Accepted: September 2001     

非阻塞同步在嵌入式操作系统中的实现

提出了把非阻塞同步机制应用于嵌入式操作系统的新设想,同时通过修改嵌入式操作系统内核源码的方法对其进行了实现。针对内核中共享资源的不同特点,综合使用了锁自由和等待自由两种不同性质的非阻塞同步策略,同时改进了锁自由的同步算法,并对原有的等待自由同步算法进行简化,使新内核具有较小的同步开销和较好的实时性能。     

A general technique for proving lock-freedom

Lock-freedom is a property of concurrent programs which states that, from any state of the program, eventually some process will complete its operation. Lock-freedom is a weaker property than the usual expectation that eventually all processes will complete their operations. By weakening their completion guarantees, lock-free programs increase the potential for parallelism, and hence make more efficient use of multiprocessor architectures than lock-based algorithms. However, lock-free algorithms, and reasoning about them, are considerably more complex.In this paper we present a technique for proving that a program is lock-free. The technique is designed to be as general as possible and is guided by heuristics that simplify the proofs. We demonstrate our theory by proving lock-freedom of two non-trivial examples from the literature. The proofs have been machine-checked by the PVS theorem prover, and we have developed proof strategies to minimise user interaction.     

无锁编程的探索与研究

在计算机多核技术迅速发展的时代,线程的优势越来越明显,多线程的学习成为每个程序员必备的基础。但在实际开发过程中,越来越多的异常,越来越多的死锁现象让每个程序员崩溃不已,线程与锁的问题凸显在每个程序员的面前。加锁技术大量应用于多线程技术的开发中,但由于加锁技术较为复杂,且调试困难,程序员们更加期望从另一个角度来缓解问题。Lock-free概念应运而生。     

基于无锁队列算法的报文分发流水线模型

本文提出一种报文分发的流水线模型,该模型中的共享数据缓冲区操作采用了动态内存分配的无锁队列算法。该算法以链表形式组织队列,避免了采用循环数组结构引起的缓冲区长度限制和内存浪费;与通用的链表队列算法相比具有实现简洁,执行效率更高,并在试验环境下验证了其性能指标。     

A dynamic-sized nonblocking work stealing deque

The non-blocking work-stealing algorithm of Arora, Blumofe, and Plaxton (hencheforth ABP work-stealing) is on its way to becoming the multiprocessor load balancing technology of choice in both industry and academia. This highly efficient scheme is based on a collection of array-based double-ended queues (deques) with low cost synchronization among local and stealing processes. Unfortunately, the algorithm's synchronization protocol is strongly based on the use of fixed size arrays, which are prone to overflows, especially in the multiprogrammed environments for which they are designed. This is a significant drawback since, apart from memory inefficiency, it means that the size of the deque must be tailored to accommodate the effects of the hard-to-predict level of multiprogramming, and the implementation must include an expensive and application-specific overflow mechanism. This paper presents the first dynamic memory work-stealing algorithm. It is based on a novel way of building non-blocking dynamic-sized work stealing deques by detecting synchronization conflicts based on “pointer-crossing” rather than “gaps between indexes” as in the original ABP algorithm. As we show, the new algorithm dramatically increases robustness and memory efficiency, while causing applications no observable performance penalty. We therefore believe it can replace array-based ABP work stealing deques, eliminating the need for application-specific overflow mechanisms. This work was conducted while Yossi Lev was a student at Tel Aviv University, and is derived from his MS thesis [1].