Search Results

Documents authored by Feng, Yueyang

Artifact
Software
DOI: 10.4230/artifacts.26388
Linearizability Hoare Logic

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

Abstract
Cite as

Eashan Hatti, Arthur Oliveira Vale, Zhongye Wang, Yueyang Feng, Zhong Shao. Linearizability Hoare Logic (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26388,
   title = {{Linearizability Hoare Logic}}, 
   author = {Hatti, Eashan and Oliveira Vale, Arthur and Wang, Zhongye and Feng, Yueyang and Shao, Zhong},
   note = {Software, NSF 2019285, NSF 2313433, NSF 2442888, DARPA Agreement No. HR00112590130, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:ee421dd7fa7166ad053af08aa59a2cf82c194b33;origin=https://github.com/ehatti/LHL;visit=swh:1:snp:bc2d555c4751e88356fa8f9419a0602643b1ef4a;anchor=swh:1:rev:453eb75c3bb4fa3812a951c762f0100b174cc7bb}{\texttt{swh:1:dir:ee421dd7fa7166ad053af08aa59a2cf82c194b33}} (visited on 2026-06-25)},
   url = {https://github.com/ehatti/LHL/tree/ecoop-camera-ready},
   doi = {10.4230/artifacts.26388},
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2026.11
A Complete Program Logic for Compositional Linearizability

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

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 11:1-11:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{hatti_et_al:LIPIcs.ECOOP.2026.11,
  author =	{Hatti, Eashan and Oliveira Vale, Arthur and Wang, Zhongye and Feng, Yueyang and Shao, Zhong},
  title =	{{A Complete Program Logic for Compositional Linearizability}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{11:1--11:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.11},
  URN =		{urn:nbn:de:0030-drops-261075},
  doi =		{10.4230/LIPIcs.ECOOP.2026.11},
  annote =	{Keywords: Program Logic, Rely-Guarantee, Linearizability, Compositional Verification, Concurrency}
}
Document
Artifact
DOI: 10.4230/DARTS.12.1.5
A Complete Program Logic for Compositional Linearizability (Artifact)

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

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

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

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)

Copy BibTex To Clipboard

@Article{hatti_et_al:DARTS.12.1.5,
  author =	{Hatti, Eashan and Oliveira Vale, Arthur and Wang, Zhongye and Feng, Yueyang and Shao, Zhong},
  title =	{{A Complete Program Logic for Compositional Linearizability (Artifact)}},
  pages =	{5:1--5:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Hatti, Eashan and Oliveira Vale, Arthur and Wang, Zhongye and Feng, Yueyang and Shao, Zhong},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.5},
  URN =		{urn:nbn:de:0030-drops-261428},
  doi =		{10.4230/DARTS.12.1.5},
  annote =	{Keywords: Program Logic, Rely-Guarantee, Linearizability, Compositional Verification, Concurrency}
}
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