README.md 1013 Bytes
Newer Older
Simon Friis Vindum's avatar
Simon Friis Vindum committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
# 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.