Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects

TL;DR

This paper proposes using Hoare-style program logics as a uniform, compositional approach for specifying and verifying non-linearizable concurrent objects and their clients, demonstrated through case studies and mechanical proofs.

Contribution

It introduces a systematic method to specify and verify various relaxed correctness conditions for concurrent objects using Hoare-style logics, enabling compositional reasoning and formal verification.

Findings

Successfully specified non-linearizable objects with Hoare-style logic

Verified concurrent client scenarios mechanically in Coq

Captured correctness conditions like linearizability and quiescent consistency

Abstract

Designing scalable concurrent objects, which can be efficiently used on multicore processors, often requires one to abandon standard specification techniques, such as linearizability, in favor of more relaxed consistency requirements. However, the variety of alternative correctness conditions makes it difficult to choose which one to employ in a particular case, and to compose them when using objects whose behaviors are specified via different criteria. The lack of syntactic verification methods for most of these criteria poses challenges in their systematic adoption and application. In this paper, we argue for using Hoare-style program logics as an alternative and uniform approach for specification and compositional formal verification of safety properties for concurrent objects and their client programs. Through a series of case studies, we demonstrate how an existing program logic for concurrency can be employed off-the-shelf to capture important state and history invariants, allowing one to explicitly quantify over interference of environment threads and provide intuitive and expressive Hoare-style specifications for several non-linearizable concurrent objects that were previously specified only via dedicated correctness criteria. We illustrate the adequacy of our specifications by verifying a number of concurrent client scenarios, that make use of the previously specified concurrent objects, capturing the essence of such correctness conditions as concurrency-aware linearizability, quiescent, and quantitative quiescent consistency. All examples described in this paper are verified mechanically in Coq.