`pthreadSignals`: Investigate using `MCPAccess.may_race` instead of only `MHP`

[michael-schwarz]

Potentially this can be made more precise by using the logic we use for barriers (and now also for ghost phase transitions).

The thing that I am unclear about is how this interacts with the lockset analysis (wait temporarily relinquishes the mutex, but I'm not sure if our lockset analysis considers this).

If it can be made more precise, we might also think about adding a second function mhp to the A module that would be answered with top by those analysis that only speak about specific memory locations.
This would allow us to stop abusing may_race with PointAccess queries in all those places where it's not about races (deadlocks comes to mind)

[michael-schwarz]

We should probably also rename our MHP analysis to CreateJoinMHP or something, as it considers only thread creations and thread joins as sources of MHP information.

The real MHP is MCPAccess.A.may_race with two PointAccess values. It's just that privatizations want to use the thread-based information only.

[sim642]

The access and MHP modules are misnomers by now indeed because we've generalized things and started using them more broadly than just races. But I think the refactoring/renaming/reshuffling can be done after we've figured out the various new ways we want to use them.

For example, I've always wanted the ad hoc MHP reasoning in useAfterFree analysis to also be extracted. It obviously doesn't fit the current may_race but it might fit some kind of may_happen_before or must_happen_before predicate which themselves could be reused more broadly. Strictly speaking, that's not MHP anymore but some of our MHP-related analyses can also be used for such queries.

[michael-schwarz]

some kind of may_happen_before or must_happen_before predicate

#1913 also uses introduces and relies on such predicates.