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.