Analysis of pthread_barriers
#1652
Conversation
|
Turns out OS X does not support barriers. |
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
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. |
|
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. |
|
Apparently mathematicians call this problem the |
|
This now uses |
michael-schwarz
force-pushed
the
issue_1651
branch
from
997ff24 to
844f3ed
Compare
|
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 |
|
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
left a comment
sim642
left a comment
There was a problem hiding this comment.
This is only a brief look, I didn't yet look at the analysis or the content of the tests.
michael-schwarz
force-pushed
the
issue_1651
branch
from
88b51a2 to
e62092e
Compare
michael-schwarz
force-pushed
the
issue_1651
branch
from
ee05d29 to
c6f23fd
Compare
michael-schwarz
force-pushed
the
issue_1651
branch
from
c6f23fd to
6caafab
Compare
Co-authored-by: Simmo Saan <[email protected]>
Co-authored-by: Simmo Saan <[email protected]>
sim642
left a comment
sim642
left a comment
There was a problem hiding this comment.
The barrierception is really nice now!
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_onceto also fit (potentially in a reduced fashion)).Technically, it accumulates the$$||_{\mathcal{A}}$$ is true pairwise among these, as well as with the caller to
capacityandMHPinformation for all calls towaitfor each barrier at a global unknown, and checks upon a call towaitthat there are at leastmin(capacity)-1other accesses wherewait.TODO:
min(capacity)-1elements whereCloses #1651.