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/vsyncer

https://github.com/hernanponcedeleon/Dat3M

https://github.com/MPI-SWS/genmc