Contextual Refinement of the Michael-Scott Queue (Proof Pearl)
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 Pre-print Media Attached | ||
17:15 - 17:30 Talk | Reasoning About Monotonicity in Separation Logic CPP Pre-print Media Attached |