A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability

We introduce simple, universal, sound, and complete proof methods for producing machine-verifiable proofs of linearizability and strong linearizability. Universality means that our method works for any object type; soundness means that an algorithm can be proved correct by our method only if it is l...

Full description

Saved in:
Bibliographic Details
Published in:Proceedings of ACM on programming languages 2024-01, Vol.8 (POPL), p.2456-2484, Article 82
Main Authors: Jayanti, Prasad, Jayanti, Siddhartha, Yavuz, Ugur, Hernandez, Lizzie
Format: Article
Language:English
Subjects:
Concurrent algorithms
Formal methods and theory of security
Logic and verification
Program verification
Security and privacy
Theory of computation
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We introduce simple, universal, sound, and complete proof methods for producing machine-verifiable proofs of linearizability and strong linearizability. Universality means that our method works for any object type; soundness means that an algorithm can be proved correct by our method only if it is linearizable (resp. strong linearizable); and completeness means that any linearizable (resp. strong linearizable) implementation can be proved so using our method. We demonstrate the simplicity and power of our method by producing proofs of linearizability for the Herlihy-Wing queue and Jayanti’s single-scanner snapshot, as well as a proof of strong linearizability of the Jayanti-Tarjan union-find object. All three of these proofs are machine-verified by TLAPS (the TLA+ Proof System).
ISSN:2475-1421
2475-1421
DOI:10.1145/3632924