A formal reduction for lock-free parallel algorithms

On shared memory multiprocessors, synchronization often turns out to be a performance bottleneck and the source of poor fault-tolerance. Lock-free algorithms can do without locking mechanisms, and are therefore desirable. Lock-free algorithms are hard to design correctly, however, even when apparently straightforward. We formalize a methodology 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 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. However, for large objects, the approach is not very attractive as the burden of copying the data can be very heavy. We propose two improved lock-free algoritms for large objects in which slower processes don't need to copy the entire object again if their attempts fail. This results in lower copying overhead than in a previous proposal.