Document Open Access Logo

A Complete Program Logic for Compositional Linearizability (Artifact)

Authors Eashan Hatti , Arthur Oliveira Vale , Zhongye Wang , Yueyang Feng , Zhong Shao

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.12.1.5.pdf
  • Filesize: 491 kB
  • 2 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Computing methodologies → Concurrent computing methodologies
  • Theory of computation → Programming logic
Keywords
  • Program Logic
  • Rely-Guarantee
  • Linearizability
  • Compositional Verification
  • Concurrency

Metrics

Artifact

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2026 Call for Artifacts and the ACM Artifact Review and Badging Policy.

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. a more general criterion, compositional linearizability, which subsumes all three criteria. We showcase the expressivity of LHL by verifying an exchanger with a set linearizable specification, the elimination-backoff stack built above the exchanger, a lock with an atomic linearized specification, and a write-snapshot object with an interval linearizable specification.
Together with LHL we formalize a modular verification framework for concurrent components based on the theory of compositional linearizability. This allows us to specify components at a high level of abstraction and granularity, and then assemble them into large systems that are correct by construction. As a showcase, we verify the elimination-backoff stack modularly by verifying each of its sub-components against their linearized specifications and then linking them together.

Cite As Get BibTex

Eashan Hatti, Arthur Oliveira Vale, Zhongye Wang, Yueyang Feng, and Zhong Shao. A Complete Program Logic for Compositional Linearizability (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/DARTS.12.1.5

Author Details

Eashan Hatti
  • Yale University, New Haven, CT, USA
Arthur Oliveira Vale
  • Yale University, New Haven, CT, USA
Zhongye Wang
  • Yale University, New Haven, CT, USA
Yueyang Feng
  • Yale University, New Haven, CT, USA
Zhong Shao
  • Yale University, New Haven, CT, USA

Funding

This work is supported in part by NSF grants 2019285, 2313433, 2442888, and by the Defense Advanced Research Projects Agency (DARPA) under Agreement No. HR00112590130. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the funding agencies.

Related Article

  • Eashan Hatti, Arthur Oliveira Vale, Zhongye Wang, Yueyang Feng, and Zhong Shao, "A Complete Program Logic for Compositional Linearizability", in 40th European Conference on Object-Oriented Programming (ECOOP 2026), LIPIcs, Vol. 372, pp. 11:1-11:28, 2026. https://doi.org/10.4230/LIPIcs.ECOOP.2026.11
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact