Bart Jacobs and Frank Piessens
Modular full functional specification and verification of lock-free data structures
We propose an approach for specifying and verifying full functional (partial) correctness of modules of multithreaded imperative programs that implement or use lock-free data structures for inter-thread communication. The approach extends separation logic with simple atomic spaces, which are regions of memory that may be accessed concurrently using atomic operations. A fixed invariant is associated with each atomic space. The specification of an atomic operation consists of the usual precondition and postcondition, as well as a number of proof obligations. The precondition requires permission to access an atomic space. The proof obligations state that, in the specific context of the call, the atomic space's invariant can be rewritten to separate out the lock-free data structure, and that updating the data structure preserves the invariant. To allow threads to retain information about the state of the data structure, a combination of fractional permissions and ghost cells is used in a way similar to the use of auxiliary variables in Owicki-Gries reasoning.
The approach has been implemented in the VeriFast program verifier, and used to verify an implementation and a client program of a multiple-enqueueer, single-dequeueer lock-free queue.report.pdf (252K) / mailto: B. Jacobs