Verifying Wait-Freedom for Concurrent Higher-Order Programs (Artifact)

Abstract

Wait-freedom is the strongest non-blocking progress guarantee for concurrent data structures, ensuring that every operation completes in a finite number of steps regardless of interference from other threads. While verification of wait-freedom has been studied for first-order languages, verifying it for higher-order programming languages with general references remains an open challenge. In such languages, operations may be used by arbitrary, unverified higher-order clients, making it unclear how to even define wait-freedom formally in terms of programs' semantics, let alone prove it.
In this paper, we present the first framework for verifying wait-freedom of concurrent programs written in a higher-order language with general references. Our approach is based on the Lawyer concurrent separation logic which has been recently introduced for termination verification. We identify a specification pattern in the Lawyer logic that captures wait-freedom. To establish this connection formally, we extend Lawyer with a novel adequacy theorem that proves that programs which are proven correct in the Lawyer logic against a specification in this aforementioned specification pattern are wait-free. Proving wait-freedom requires us to show that all calls made to operations by any arbitrary client terminate. Thus, as part of formally proving wait-freedom, i.e., as part of the proof of the adequacy theorem above, we need to prove that the behavior of the client of the data structure is safe in the sense that it does not break the internal invariants of the data structure, e.g., by directly manipulating the data structure’s internal state. To this end, we develop a logical relations model that establishes safety for all clients once and for all.
We demonstrate the effectiveness of our approach by proving wait-freedom for several representative examples, including higher-order functions such as the list map function, and a memory-efficient single-producer, single-consumer queue. For the latter, wait-freedom is conditional in that as the name suggests there can be at most one enqueuer thread and one dequeuer thread. To capture this formally we introduce the notion of restricted wait-freedom as a variant of wait-freedom that restricts the number of concurrent threads, and show how our approach can support reasoning about restricted wait-freedom. All our results have been mechanized on top of the Rocq Prover and using the Iris separation logic framework that Lawyer is also based on.