Comment Comment by ricudis There is quite a lot of research work in formally proving correctness of such primitives in relaxed-order memory architectures. You might want to take a look in some of them:https://github.com/open-s4c/vsyncerhttps://github.com/hernanponcedeleon/Dat3Mhttps://github.com/MPI-SWS/genmc parent ricudis 20 days ago
https://github.com/open-s4c/vsyncer
https://github.com/hernanponcedeleon/Dat3M
https://github.com/MPI-SWS/genmc