This is joint work with Gao Hui (Groningen University). It concerns
two papers
Lock-free algorithms can do without locking mechanisms, and are therefore desirable. A true problem of lock-free algorithms is that they are hard to design correctly, even when apparently straightforward. We formalize Herlihy's methodology [1] for transferring a sequential implementation of any data structure into a lock-free synchronization by means of synchronization primitives Load-linked (LL)/store-conditional (SC). This is done by means of a reduction theorem that enables us to reason about the general lock-free algorithm to be designed on a higher level than the synchronization primitives. The reduction theorem is based on refinement mapping as described by Lamport [2] and has been verified with the higher-order interactive theorem prover PVS. Using the reduction theorem, fewer invariants are required and some invariants are easier to discover and easier to formulate.
The lock-free implementation works quite well for small objects. The approach is less attractive for large objects, since the burden of copying the data can be very heavy. We propose two enhanced lock-free algorithms for large objects using partial copying. They seem particularly effective since the slower processes don't need to copy the entire object again if their attempts fail. This results in lower copying overhead than in Herlihy's proposal.
To ensure our hand-written proof presented in the paper is not flawed, we use the higher-order interactive theorem prover PVS for mechanical support. All associated PVS theories and proof scripts can be downloaded here.
The compare-and-swap register (CAS) is a synchronization primitive for lock-free algorithms. Most uses of it, however, suffer from the so-called ABA problem. The simplest and most efficient solution to the ABA problem is to include a tag with the memory location such that the tag is incremented with each update of the target location. However, applying this solution is not theoretically bug-free and limits their applicability. This paper presents a general lock-free pattern that is based on synchronization primitive CAS without causing ABA problem or problems with wrap around. It can be used to provide lock-free functionality for any generic data type.
Our algorithm is a CAS variation of Herlihy's LL/SC methodology for lock-free transformation. The basis of our techniques is to poll different locations on reading and writing objects, in such a way that the consistency of an object can be checked by its location instead of its tag. It consists of very simple code that can be easily implemented using C-like languages.
A true problem of lock-free algorithms is that they are hard to design correctly, which even holds for apparently straightforward algorithms. We therefore develop a reduction theorem that enables us to reason about the general lock-free algorithm to be designed on a higher level than the synchronization primitives. The reduction theorem is based on refinement mapping as described by Lamport [2] and has been verified with the higher-order interactive theorem prover PVS. Using the reduction theorem, fewer invariants are required and some invariants are easier to discover and formulate without considering the internal structure of the final implementation.All associated PVS theories and proof scripts can be downloaded here.
Comments are welcome, 5 July 2006.
Back to my home page.
Wim H. Hesselink, e-mail: wim@cs.rug.nl