A port of Peterson's 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 paper, available online, 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 iris!775 (closed) per request