# Michael Scott queueThe Michael-Scott queue (MS-queue) is a fast and practical concurrent queue. Inthis example we prove that both the original MS-queue, and variant of it, is acontextual refinement of a queue implemented using course grained concurrency.The variant of the MS-queue closely resembles `ConcurrentLinkedQueue` in theJava standard library `java.util.concurrent`.For a more detailed description of the queue and the proofs see the notes [Proofof Contextual Refinement of Michael-Scott Queue using Logical Relations inIris](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.