Aarhus University Seal / Aarhus Universitets segl

Contextual refinement of the Michael-Scott queue (proof pearl)

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

DOI

The Michael-Scott queue (MS-queue) is a concurrent non-blocking queue. In an earlier pen-and-paper proof it was shown that a simplified variant of the MS-queue contextually refines a coarse-grained queue. Here we use the Iris and ReLoC logics to show, for the first time, that the original MS-queue contextually refines a coarse-grained queue. We make crucial use of the recently introduced prophecy variables of Iris and ReLoC. Our proof uses a fairly simple invariant that relies on encoding which nodes in the MS-queue can reach other nodes. To further simplify the proof, we extend separation logic with a generally applicable persistent points-to predicate for representing immutable pointers. This relies on a generalization of the well-known algebra of fractional permissions into one of discardable fractional permissions. We define the persistent points-to predicate entirely inside the base logic of Iris (thus getting soundness "for free"). We use the same approach to prove refinement for a variant of the MS-queue resembling the one used in the java.util.concurrent library. We have mechanized our proofs in Coq using the formalizations of ReLoC and Iris in Coq.

Original languageEnglish
Title of host publicationCPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs
Editors Cătălin Hriţcu, Andrei Popescu
Number of pages15
Place of publicationNew York
PublisherAssociation for Computing Machinery
Publication yearJan 2021
Pages76-90
ISBN (print)978-1-4503-8299-1
DOIs
Publication statusPublished - Jan 2021
Event10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021 - Virtual, Online, Denmark
Duration: 17 Jan 202119 Jan 2021

Conference

Conference10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, co-located with POPL 2021
LandDenmark
ByVirtual, Online
Periode17/01/202119/01/2021
SponsorACM SIGPLAN

Bibliographical note

Publisher Copyright:
© 2021 ACM.

    Research areas

  • Concurrency, Coq, Iris, Separation logic

See relations at Aarhus University Citationformats

ID: 219447097