Analysis of pthread_barriers

[michael-schwarz]

Makes use of the $$||_{\mathcal{A}}: \mathcal{A} \to \mathcal{A} \to \{ \textsf{false},\top \}$$ predicate we want to define for (abstract) digests to provide a sound basis for all of our MHP stuff for races and give a principled account of what I added in #518 .

Interestingly, it even does so outside of the context of data races --- which may be a cute insight on top of putting the race analysis on solid foundations with this predicate (and hopefully finding a way to get pthread_once to also fit (potentially in a reduced fashion)).

Technically, it accumulates the capacity and MHP information for all calls to wait for each barrier at a global unknown, and checks upon a call to wait that there are at least min(capacity)-1 other accesses where $$||_{\mathcal{A}}$$ is true pairwise among these, as well as with the caller to wait.

TODO:

• Use TIDs and Joins
• Use further abstract digests (such as must-lockset digest)
• Use information also for excluding races (beyond unreachability)
• Come up with a less expensive algorithm for checking there are min(capacity)-1 elements where $$||_{\mathcal{A}}$$ holds pairwise ?
• Handle barriers configured for inter-process communication soundly by not doing anything for them

Closes #1651.

[michael-schwarz]

OS X CI does OS X things, I'll just ignore that for now.

Turns out OS X does not support barriers.

[michael-schwarz]

Come up with a less expensive algorithm for checking there are min(capacity)-1 elements where $$||_{\mathcal{A}}$$ holds pairwise ?

Does anyone have an idea how this could be done? I'm not sure if one can do better complexity-wise, but it should be possible at least w.r.t. the constants.

[michael-schwarz]

I talked it through with @DrMichaelPetter and we came up with some dynamic programming-like algorithm that hopefully performs better practically, but neither of us see how one can do better complexity wise.

[michael-schwarz]

Apparently mathematicians call this problem the Admissible Subset Selection Problem. But looking around a bit, I have not found an algorithm that would help solve the problem.

[michael-schwarz]

This now uses Seq to hopefully avoid constructing the full product every single time.