From 45704cf0399e68742b0a490ca8a8e6869fce2634 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Thu, 11 Jun 2020 11:20:14 +0200 Subject: [PATCH] Add readme --- .../F_mu_ref_conc/examples/queue/README.md | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 theories/logrel/F_mu_ref_conc/examples/queue/README.md diff --git a/theories/logrel/F_mu_ref_conc/examples/queue/README.md b/theories/logrel/F_mu_ref_conc/examples/queue/README.md new file mode 100644 index 0000000..e2be9f0 --- /dev/null +++ b/theories/logrel/F_mu_ref_conc/examples/queue/README.md @@ -0,0 +1,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. \ No newline at end of file -- GitLab