Formal Verification of Chase-Lev Deque in Concurrent Separation Logic

TL;DR

This paper presents a formal, mechanized verification of the Chase-Lev deque data structure in concurrent separation logic, ensuring correctness, safety, and strong specifications in a realistic, unbounded, and relaxed memory environment.

Contribution

It provides the first comprehensive formal verification of the Chase-Lev deque using a minimal trusted base and realistic implementation, including support for safe memory reclamation.

Findings

Verified the Chase-Lev deque in Coq with a strong linearizability specification.

Extended verification to include safe memory reclamation.

Laid groundwork for verifying the deque under relaxed memory models.

Abstract

Chase-Lev deque is a concurrent data structure designed for efficient load balancing in multiprocessor scheduling. It employs a work-stealing strategy, where each thread possesses its own work-stealing deque to store tasks, and idle threads steal tasks from other threads. However, given the inherent risk of bugs in software, particularly in a multiprocessor environment, it is crucial to formally establish the correctness of programs and data structures. To our knowledge, no formal verification work for the Chase-Lev deque has met three key criteria: (1) utilizing a minimal trusted computing base, (2) using a realistic and unrestricted implementation, and (3) proving a strong specification. In this thesis, we address this gap by presenting the formal verification of the Chase-Lev deque using a concurrent separation logic. Our work is mechanized in the Coq proof assistant, and our verified implementation is both realistic and unbounded in terms of the number of tasks it can handle. Also, we adopt linearizability as the specification, as it is widely recognized as a strong specification for concurrent data structures. Consequently, our work satisfies all three aforementioned criteria for formal verification. Additionally, we extend our verification to support safe memory reclamation, and provide a basis for verifying the Chase-Lev deque in the relaxed memory model.