ReLoC merge requestshttps://gitlab.rts.mpi-sws.org/iris/reloc/-/merge_requests2022-08-28T08:17:43Zhttps://gitlab.rts.mpi-sws.org/iris/reloc/-/merge_requests/7Prove weakening for `typed`2022-08-28T08:17:43ZPaolo G. GiarrussoProve weakening for `typed`Part of an answer to an Iris HelpDesk question — see https://mattermost.mpi-sws.org/iris/pl/m64hgftb8ffpmbdhnxkoo7ga8r.Part of an answer to an Iris HelpDesk question — see https://mattermost.mpi-sws.org/iris/pl/m64hgftb8ffpmbdhnxkoo7ga8r.https://gitlab.rts.mpi-sws.org/iris/reloc/-/merge_requests/4WIP: Add Michael Scott queue2020-09-10T18:44:21ZSimon Friis VindumWIP: Add Michael Scott queueAdds 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_...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.Dan FruminDan Frumin