The Design and Verification of Dynamic-sized Nonblocking Data Structures

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.