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.

[sim642]

By the way, @jprotopopov-ut was doing some Linux kernel stubbing using barriers and I mentioned this PR, but I don't know if this ended up being used/useful there.

[jprotopopov-ut]

By the way, @jprotopopov-ut was doing some Linux kernel stubbing using barriers and I mentioned this PR, but I don't know if this ended up being used/useful there.

It did not work properly, but I did not spend any time to investigate the reasons and instead ended up implementing ad-hoc barriers using a set of atomic flags

[michael-schwarz]

What do you mean it wasn't working properly? Was it unsound (would be worth investigating) or just not precise enough for your case (that is expected from time to time)?

[jprotopopov-ut]

What do you mean it wasn't working properly? Was it unsound (would be worth investigating) or just not precise enough for your case (that is expected from time to time)?

As far as I remember, it was too imprecise, but I didn't notice any soundness issues. However, it was only a quick test, and I could have probably missed some things

[sim642]

This is only a brief look, I didn't yet look at the analysis or the content of the tests.

[sim642]

The barrierception is really nice now!

[sim642]

This seems irrelevant here, there's no other access of g anyway. The test is about the checks.