Formal verification of concurrent lists in concurrent separation logic

Abstract

Concurrent sets are a fundamental building block of various programs running on multithreaded systems. The most important concurrent set is Harris's list, a lock-free linked list that introduced many key ideas in concurrent set design. Such concurrency allows for highly performant programs, but it also introduces a much higher risk of bugs. Hence, it is important to formally verify the correctness of concurrent sets, in particular of Harris's list. However, there is no work on proving Harris's list that proved a strong specification, is foundational with a minimal trusted computing base, and properly handles memory reclamation at the same time. In this thesis, we present a formal verification of Harris's list in the concurrent separation logic Iris. We prove the linearizability of Harris's list, the de facto correctness criterion for concurrent data structures. All of our work is mechanized in the Coq proof assistant, providing a proof that is done with a minimal trusted computing base. Our implementation handles memory reclamation by utilizing RCU, a safe memory reclamation scheme that is widely used in concurrent data structures. Thus, this thesis presents the first proof of Harris's list that satisfied all of the aforementioned properties.