WIP: MS-queue
This MR adds an additional example to the logrel development: A proof that the Michael-Scott queue, and a variant of it, is a refinement of a course-grained queue.
I've marked the MR WIP as it, at least, needs to be updated with a link to the accompanying notes (they are not hosted anywhere yet, but a draft is here). Additionally, I have an MR with the same proof, but based on ReLoC, here and any feedback on one is probably also applicable to the other.
The MR also makes a few small changes to some of the existing examples better adapting them to changes that have happened in Iris.
Merge request reports
Activity
1 # Michael Scott queue 2 3 The Michael-Scott queue (MS-queue) is a fast and practical concurrent queue. In 4 this example we prove that both the original MS-queue, and variant of it, is a 5 contextual refinement of a queue implemented using course grained concurrency. 6 The variant of the MS-queue closely resembles `ConcurrentLinkedQueue` in the 7 Java standard library `java.util.concurrent`. 8 9 For a more detailed description of the queue and the proofs see the notes [Proof 10 of Contextual Refinement of Michael-Scott Queue using Logical Relations in 11 Iris](FIXME INSERT LINK TO NOTES). 648 { iNext. iExistsFrame. } 649 iModIntro. 650 clear m. 651 iApply wp_pure_step_later; auto. iNext. 652 iApply wp_value. simpl. 653 iApply wp_pure_step_later; auto. iNext. simpl. 654 iApply wp_value. 655 iApply wp_pure_step_later; auto. iNext. 656 iApply wp_value. 657 simpl. 658 (* Currently ℓlast is both the tail we read and the node we're looking at. 659 This is not going to be the case when we want to use the IH. Therefore 660 we have to generalize the goal such that we "split" occurences of 661 ℓlast. *) 662 iAssert (node_mapsto κ ℓlast ι ℓpt) as "nextMapsto". iAssumption. 663 generalize ℓlast at 2 3 4 5 6 8 9 10 11. iIntros (ℓnext). 
-
The MR also makes a few small changes to some of the existing examples better adapting them to changes that have happened in Iris.
This could conflict badly with !38 (merged), so maybe it's better to factor these out into a separate MR?
-
@simonfv what is the status of this? I haven't looked at the code in detail yet, but I think it would make sense to separate the drive-by fixes. I can make time to do a rough scan over the code, but we'll probably not do a detailed review given the amount of code and that it is "just" for examples -- but we still need to be able to maintain it to keep it working with newer Iris.
-
@simonfv Thanks for this MR! I am going to close it for now to indicate that it is not actively being worked on (I know it is marked WIP, but if we collect everyone's WIP in open MRs, we'll quickly drown in non-actionable items in the MR list). If you ever want to come back to this and complete the missing bits you noted yourself, please re-open. :) Also see above for some comments I had for this MR.