Avoid spurious writes for invariants in base mutex-meet-tid

[sim642]

While describing the special invariant writes to globals for my thesis, I looked through all of the write_global implementations and noticed that some mutex-meet variants do not use the optimization:

• base mutex-meet-tid,
• relation mutex-meet,
• relation mutex-meet-tid.

I have quickly added a test for base mutex-meet-tid which reveals precision loss from such spurious side effects. The PR also includes a quick fix for it by analogy, but I haven't thought about it much nor properly tested it.

If this is sound, then we should probably have this since it can improve both precision and performance.

[michael-schwarz]

I'm not sure it is strictly an optimization unfortunately. I think the reason it is not done some of the times is code such as

lock(a);
g = ?;
while(g < 20)  { };
unlock(a);

which occurs quite a few times in SV-COMP snippets as assume_abort_if_not or similar. Here, it may be beneficial to actually consider this a write and later cause a side-effect and add it to LMust.

However, it should still be sound, so maybe we should just try to add it everywhere and then benchmark again?

[sim642]

Looks like mutex-meet-tid is the only privatization where W not only determines side effects and local state change at unlock but also changes other data structures (i.e., LMust).
Perhaps changing W from a set to a map with may-boolean values would allow retaining such precision as well. write_global would add not invariant to W for g and unlock would only side effect those with true, while adding all of them to LMust (and I guess L as well?)

[michael-schwarz]

Addings thing to LMust while not causing a side-effect breaks the invariant about what LMust means though, and could lead to issues similar to the soundness problem you remarked we had in #1643.

[sim642]

What invariant about LMust? It seems that LMust is just used to decide whether initial values should be joined in or not. But initial values are not the ones that would be side-effected at write_global/unlock.
The abstract values from invariant writes are refinements from what would be read anyway, so the lack of such side effect should not be a problem. Not doing any invariant writes (and thus not having the corresponding side effects) would also be sound, just globals cannot be refined at all then.

If the current version is sound and the version in this PR is sound, then their meet should be as well. Since almost everything is shared between the two, it should be possible to merge the two together, e.g. having the different W from both variants at hand where needed.