genmc vs IMM paper (Remark 2) about genmc HOT 3 CLOSED

Hi Hernan,

genmc -imm does not follow the published IMM model to the letter: it uses the same sw definition as RC11. Going forward, since C++20 adopted a stronger definition of release sequences, we should probably update both RC11 and IMM to adopt the C++20 definition.

You are right about the acquire tag in (2, 3): UWacq (x, 2) L.20. It is there because the FAI is marked "acq" but is effectively ignored: UWacq is treated exactly as a UWrlx.

from genmc.

Thanks @vafeiadis for the clarification. Is there any other difference between the implemented model and the paper? What about the strong RMW instructions (like example 3.10). It seems to me that genmc understands all writes coming from a RMW as a strong one. Is this correct?

from genmc.

What about the strong RMW instructions (like example 3.10). It seems to me that genmc understands all writes coming from a RMW as a strong one. Is this correct?

This is currently the case, yes.

Is there any other difference between the implemented model and the paper?

I don't recall any other differences (apart from GenMC supporting SC accesses and IMM not). I am closing this for now, but will post here any other changes to the model.

from genmc.