A Complete Program Logic for Compositional Linearizability
Last modified: Tue Apr 28 09:01:44 2026 GMT.
Authors
Eashan HattiArthur Oliveira Vale
Zhongye Wang
Yueyang Feng
Zhong Shao
Abstract
We present Linearizability Hoare Logic (LHL), the first mechanized, sound and complete program logic for atomic, set, and interval linearizability. We achieve this by showing soundness and completeness of LHL w.r.t. to a more general criterion, compositional linearizability, which subsumes all three criteria. We showcase the range of expressivity of LHL by verifying an exchanger with a set linearizable specification, the eimination-backoff stack built above the exchanger, a lock with an atomic linearized specification, and a write-snapshot object with an interval linearizable specification.LHL exists within a compositional model for concurrent computation which enables us to use the compositionality features of compositional linearizability to compose verified components together into large systems with a high-level of abstraction for its subcomponents. As a showcase, we verify the elimination-backoff stack implementation modularly by verifying all of its sub-components against their linearized specifications and then linking them together using compositional linearizability.
