# Michael Scott queue
The Michael-Scott queue (MS-queue) is a fast and practical concurrent queue. In
this example we prove that both the original MS-queue, and variant of it, is a
contextual refinement of a queue implemented using course grained concurrency.
The variant of the MS-queue closely resembles `ConcurrentLinkedQueue` in the
Java standard library `java.util.concurrent`.
For a more detailed description of the queue and the proofs see the notes [Proof
of Contextual Refinement of Michael-Scott Queue using Logical Relations in
Iris](FIXME INSERT LINK TO NOTES).
## Overview of the files.
* `common.v`: Common definitions that are identical across the two variants of
the queue.
* `MS_queue`: An implementation of both the original MS-queue and the variant.
* `CG_queue`: An implementation of a course grained queue, a linked list guarded
by a lock.
* `refinement_variant.v`: Refinement proof of the variant of the MS-queue.
* `refinement_original.v`: Refinement proof of the original MS-queue.