Abstract:
Modern computer systems often involve multiple processes or threads of control that communicate
through shared memory. However, the implementation of correct and efficient data
structures 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 the
verification of nonblocking algorithms that dynamically allocate memory. These techniques
allow the construction of formal and complete proofs of correctness, so that each proof may
be checked by a mechanical proof assistant. Applying techniques first developed for the
verification of distributed algorithms, we use labelled-transition systems to model algorithms
and their specifications, and simulation relations to prove that an implementation meets its
specification. Nonblocking algorithms often require a particular notion of simulation, called
backward simulation, that is rarely necessary in other contexts. This thesis contributes to the
relatively 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 on the availability of two powerful synchronisation primitives, known as load-linked and store-conditional, which are not normally provided by hardware. We present implementations of these primitives that
work on commonly available platforms.
