WIP: Add Michael Scott queue

Adds an additional example: A proof that the Michael-Scott queue, and a variant of it, is a refinement of a course-grained queue.

As of right now the proofs use the lemmas refines_load_alt and refines_cmpxchg_l_alt, as the refines_load and refines_cmpxchg_l in ReLoC are not strong enough. Before merging the MR I think it would make sense to decide what the best solution to that is. Should those lemmas or variants of them be added to ReLoc? Should the existing lemmas be changed? Or something else?

I've marked the MR WIP as I'll also submit a MR for iris/examples with a version of the proof that I did without using ReLoC.

assigned to @dfrumin

Thanks a lot Simon! This looks fantastic. I think that the stronger version of the load rule should be adapated. I will try to do that soon. I am not so sure about refines_cmpxchg_l_alt: could you get away without using the additional update |={E',E}=> there?

Also, could you maybe add some comments about the data structure itself: what paper is it from and what is the difference between the original and the _variant versions?

mentioned in merge request examples!37 (closed)

added 1 commit

• 1c9f6962 - Add readme

Compare with previous version

I am not so sure about refines_cmpxchg_l_alt: could you get away without using the additional update |={E',E}=> there?

Yeah, me neither. I don't think the |={E',E}=> adds any extra power/makes the rule more complete. But, for my use case, it was convenient to have since I needed to first apply the lemma, open an invariant (using the first update modality), split on the disjunction, and then do a frame-preserving update (using the second update modality).

Without it, I think I'd have to figure out if the cmpxchg fails using destruct (decide (v = v')) and then afterwards use refines_cmpxchg_l where I'd then have to eliminate the wrong cases. Doing that would be easier if there where refines_cmpxchg_suc_l and refines_cmpxchg_l and refines_cmpxchg_fail_l rules I think.

I've added a small README file.

added 17 commits

• 1c9f6962...c5a3ab55 - 10 commits from branch iris:master
• 4c76ffa4 - Add MS-queue
• c82aaff3 - Adapt to changes in ReLoC/Iris, refactor proofs
• 8a93b036 - Refactor proof, rename variables
• f7a425fd - Obtain a closed proof
• 80cbdee9 - Cleanup commented code
• f801ecd3 - Add readme
• ab4d5733 - WIP proof of the original MS-queue

Compare with previous version

added 12 commits

• ab4d5733...da7951b4 - 2 commits from branch iris:master
• 1553752e - Add MS-queue
• 473099f0 - Adapt to changes in ReLoC/Iris, refactor proofs
• 7fcfe85e - Refactor proof, rename variables
• 926e2c28 - Obtain a closed proof
• 6960e74c - Cleanup commented code
• 9c1a2de1 - Add readme
• 1a37290a - WIP proof of the original MS-queue
• c18fa555 - Finish proof of original MS-queue, one lemma admitted
• 5ffe93e2 - Remove last admit
• 5db10518 - Refactor proof to not use state disjunction for nodes

Compare with previous version

added 1 commit

• e617b8c7 - Completely new invariant and ghost state

Compare with previous version

added 1 commit

• 4915969f - Refactor

Compare with previous version

added 1 commit

• 51cc7a60 - Use persistent points-to predicate

Compare with previous version

added 29 commits

• 51cc7a60...eec78b3b - 14 commits from branch iris:master
• e1b98cfa - Add MS-queue
• d551c697 - Adapt to changes in ReLoC/Iris, refactor proofs
• 8044d853 - Refactor proof, rename variables
• dd8eb646 - Obtain a closed proof
• 04cf8981 - Cleanup commented code
• 1c1a98eb - Add readme
• e95f35e3 - WIP proof of the original MS-queue
• 09b1d9d8 - Finish proof of original MS-queue, one lemma admitted
• 3c639110 - Remove last admit
• 84c32bcc - Refactor proof to not use state disjunction for nodes
• 1e514435 - Completely new invariant and ghost state
• 6089ccba - Refactor
• a8059184 - Use persistent points-to predicate
• d3ab637a - Tweak specification for a simpler proof
• c0d7d490 - Various changes in accordance with paper proof

Compare with previous version