Add atomic fetch-and-add to `heap_lang`
For the sake of demonstrating Iris, it is often useful to have an atomic fetch-and-add instruction (see for example my TTT talk and Derek's MFPS talk). Of course, we can implement such a thing using a CAS loop, but then the proof in Coq becomes quite different from the proof on paper.
Adding an atomic fetch-and-add instruction to heap_lang should be easy, and it makes sense, since many actual architectures have such an instruction.
What do you think? Are there any other common atomic instructions that we may add too? We could add something like:
AtomicBinOp (op : bin_op) (e1 : expr) (e2 : expr).But it is a bit weird to use it with LeOp, LtOp or EqOp since those change the type of the location.