LAPOR implementation is not complete about genmc HOT 3 CLOSED

That's a good observation. However, the executions of this program are not lock-well-formed. According to the paper, LAPOR should report an error in such cases, although the implementation does not do that in practice. (I think the reason I had in mind when implementing the code was to accommodate assume() statements within critical sections, as such constructs can easily lead to not lock-well-formed executions.)

Perhaps printing at least a warning would be a better option.

from genmc.

I looked into the paper before reporting the issue, but couldn't find that constraint at the time (only that the memory model needs to be lock-extensible). I guess this sentence confused me: "That is, if the underlying memory model is well-formed,
prefix-closed and lock-extensible, then LAPOR is complete."

from genmc.

GenMC does print a warning since v0.6(?), and some spurious warnings have been fixed in v0.6.1.

from genmc.