Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis

TL;DR

This paper introduces a novel approach to verify concurrent lock-free data structures by decoupling their correctness from complex memory reclamation, enabling fully automated verification of structures like queues.

Contribution

It presents a method to verify data structures and memory management separately, simplifying the verification process and making automation feasible for complex lock-free structures.

Findings

Verified linearizability of Michael&Scott's queue

Verified DGLM queue with hazard pointers and epoch-based reclamation

First fully automatic verification of such lock-free data structures

Abstract

Verification of concurrent data structures is one of the most challenging tasks in software verification. The topic has received considerable attention over the course of the last decade. Nevertheless, human-driven techniques remain cumbersome and notoriously difficult while automated approaches suffer from limited applicability. The main obstacle for automation is the complexity of concurrent data structures. This is particularly true in the absence of garbage collection. The intricacy of lock-free memory management paired with the complexity of concurrent data structures makes automated verification prohibitive. In this work we present a method for verifying concurrent data structures and their memory management separately. We suggest two simpler verification tasks that imply the correctness of the data structure. The first task establishes an over-approximation of the reclamation behavior of the memory management. The second task exploits this over-approximation to verify the data structure without the need to consider the implementation of the memory management itself. To make the resulting verification tasks tractable for automated techniques, we establish a second result. We show that a verification tool needs to consider only executions where a single memory location is reused. We implemented our approach and were able to verify linearizability of Michael&Scott's queue and the DGLM queue for both hazard pointers and epoch-based reclamation. To the best of our knowledge, we are the first to verify such implementations fully automatically.