2026-09-26T21:32:48Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26107 2026-09-24T00:00:16Z ddc:004 open_access

A Complete Program Logic for Compositional Linearizability Hatti, Eashan Oliveira Vale, Arthur Wang, Zhongye Feng, Yueyang Shao, Zhong Program Logic Rely-Guarantee Linearizability Compositional Verification Concurrency 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Eashan Hatti and Arthur Oliveira Vale and Zhongye Wang and Yueyang Feng and Zhong Shao 2026 Is Part Of LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2026.11 urn:nbn:de:0030-drops-261075 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.11 eng https://creativecommons.org/licenses/by/4.0/legalcode