Completeness of Logical Atomicity for Linearizability in Concurrent Separation Logic

Linearizability is a standard correctness condition for concurrent data structures. It guarantees that operations behave as if they took effect at some atomic instant between their call and return points. Despite the central role linearizability plays, prior work has argued for instead using a style of specification that internalizes the atomicity of operations in terms of the logic's reasoning rules, known as logical atomicity. These logically atomic specifications are intended to be easier to compose inside of the logic than linearizability. Prior work has shown that in the Iris separation logic framework, a certain form of logically atomic specifications implies that a data structure is linearizable. However, the converse remained an open question: for every linearizable data structure, is it always possible to derive a corresponding logically atomic specification? This paper resolves this question in the affirmative. We prove a completeness theorem for Iris that derives a logically atomic specification for any linearizable data structure. As a consequence, we are able to embed a variety of linearizability proof techniques into Iris and use them to derive logically atomic specifications. We apply this to three linearizability proof methods: aspect-oriented linearizability proofs, forward simulations with commit points, and meta-configuration tracking. Using these embeddings, we derive logically atomic specifications for the Herlihy-Wing queue and the Baskets Queue. We furthermore establish a connection between logical atomicity and an encoding of refinement in Iris that has been used in prior logical relations models. This result allows us to transport logically atomic specifications across refinements, which we apply to the Folly MPMC queue implementation. All of the results in this paper have been mechanized in the Rocq Prover.