Commit 45704cf0 authored by Simon Friis Vindum's avatar Simon Friis Vindum

Add readme

parent 390663b1
# 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.
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment