Use MHP to exclude races & Refactoring MHP

[michael-schwarz]

This now uses the MHP information we compute to exclude more races.
To this end, at each access, we record a tuple of MHP information along with the access.

It also refactors some of our more-traces code by moving MHP to a separate module.

The code around race warnings should probably be looked over carefully, the PR contains a first step towards moving back to pair-wise race warnings.

[sim642]

Here's something I've wondered before: could there be any way to entirely get rid of the (labeled) string stuff from the accesses and replace them with something more type-safe (allowing for additional operations in pairwise race checking)?
Because this now adds a history-thread-IDs-specific component to the entire access structure in addition to the strings. It's not very flexible if this has to be done for every other analysis-specific race check we might have.

[michael-schwarz]

Here's something I've wondered before: could there be any way to entirely get rid of the (labeled) string stuff from the accesses and replace them with something more type-safe (allowing for additional operations in pairwise race checking)?

I have also given this some thought, but I did not find any immediately obvious solution: What one would want is some RaceInformation module.

module type RaceInformation = sig
  type t = MHP of MHP.t | Lockset of Lvalset | ...
  val may_race: t -> t -> bool
end

One would then collect sets of such things and the check for two such sets if there exists a and b such that may_race a b is false.

However, we do not really win much there as this RaceInformation thing would still have to explicitly have all possible values that could be the cause for such an exclusion....

So that doesn't seem to be it either.

[vesalvojdani]

These code changes look good. We have quite many thread analyses now.... thread, threadflag and threadJoins.