examples merge requestshttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests2022-02-07T09:29:40Zhttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/49Added petersons algorithm as an example of sequential consistency2022-02-07T09:29:40ZJonas KastbergAdded petersons algorithm as an example of sequential consistencyA port of [Peterson's algorithm](https://en.wikipedia.org/wiki/Peterson%27s_algorithm)--A CAS-free lock for a fixed number of participants (here 2), that relies on sequential consistency--to HeapLang.
This is a direct port of the impleme...A port of [Peterson's algorithm](https://en.wikipedia.org/wiki/Peterson%27s_algorithm)--A CAS-free lock for a fixed number of participants (here 2), that relies on sequential consistency--to HeapLang.
This is a direct port of the implementation and proof presented in the [Cosmo'ICFP20](https://iris-project.org/pdfs/2020-icfp-cosmo-final.pdf) paper, available [online](https://gitlab.inria.fr/gmevel/cosmo/-/blob/master/theories/examples/peterson.v), and all credit goes to the authors (Glen Mével, Jacques-Henri Jourdan, François Pottier) for the original implementation, as the port was very straightforward.
I thought that the lock was quite cute (being CAS-free), and thus could make sense to include in the library of HeapLang (for one as evidence of how its sequentially consistent nature can be used for reasoning), although it is of course up for debate.
I am willing to improve the structure/proof if need be.
NB: Moved from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/775 per requesthttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/58Add parallel add example2022-11-01T18:51:27ZJonas KastbergAdd parallel add exampleAn example based on a generalization of parallel_incr, that has also
been covered in the Iris Lecture NotesAn example based on a generalization of parallel_incr, that has also
been covered in the Iris Lecture Noteshttps://gitlab.rts.mpi-sws.org/iris/examples/-/merge_requests/59Add Chase-Lev deque2023-09-24T05:15:25ZJaemin ChoiAdd Chase-Lev dequeThis MR adds logically atomic specifications and proof of Chase-Lev work-stealing deque.
Note: the proof uses a strong variant of `mono_nat_own_alloc` and a variant of LATs having extra non-atomic postconditions, so `mono_nat.v` and `at...This MR adds logically atomic specifications and proof of Chase-Lev work-stealing deque.
Note: the proof uses a strong variant of `mono_nat_own_alloc` and a variant of LATs having extra non-atomic postconditions, so `mono_nat.v` and `atomic.v` were taken from the Iris repository and edited.