Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Mon 18 Jan 2021 17:00 - 17:15 at CPP - Program Logics Chair(s): William Mansky

The Michael-Scott (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 is a contextual refinement of a coarse-grained queue; and it has been conjectured that one would need some kind of prophecy variables to show contextual refinement for the original MS-queue. Here we use the Iris and ReLoC logics to show, for the first time, that the original MS-queue is a contextual refinement of 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. We define the persistent points-to predicate entirely inside the base logic of Iris by introducing two novel resource algebras.

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.

Mon 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

17:00 - 17:30: Program LogicsCPP at CPP
Chair(s): William ManskyUniversity of Illinois at Chicago

Streamed session: https://youtu.be/poHYVOMQuro?t=3869

17:00 - 17:15
Talk
Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
CPP
Simon Friis VindumAarhus University, Lars BirkedalAarhus University
Pre-print Media Attached
17:15 - 17:30
Talk
Reasoning About Monotonicity in Separation Logic
CPP
Amin TimanyAarhus University, Lars BirkedalAarhus University
Pre-print Media Attached