-
Notifications
You must be signed in to change notification settings - Fork 72
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add some hacky atomic privatizations #1216
Conversation
I have not looked at the implementation yet, but starting from the formal description, I started wondering for the relational privatization:
|
Yes, and they're also published at the end of the atomic section regardless of whether they remain protected by any real mutexes. So it isn't really any different from real mutexes in that sense. |
Can this not lead to imprecision when local values haven been set to top at the unlock of the last (real) protecting mutex? |
Possibly, I haven't thought about it too much and the tests are very simple. Explicitly tracking globals written under the current atomic section might avoid many of the issues. Currently I tried to get away with some existing information to see if this would work at all. |
Another interesting observation is that the Freiburg |
I cleaned this up to a state where all the privatizations with atomic block support are under separate names, not under their default names. And the unsound combination For relational analyses, there are monolithic unprotected invariants in the atomic variants. For these examples, this isn't any bottleneck. Rather we're still missing some precision, which is what we should be solving. The previous non-atomic variants use per-global unprotected invariants instead. Therefore, there should be no downside to getting these experimental privatizations merged. This is a step in the right direction. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Given that they are fairly separate from everything else, I am fine with merging as is in the interest of moving things along.
We might want to output some warning though that this analysis is still considered very experimental.
I do have some headaches with merging this:
-
At least to me this seems very ad-hoc and I would hope to get to a state where we have a principled understanding of what exactly this does (and perhaps even some soundness considerations for (a simplification of) these analyses like we have in the SAS '21 / ESOP '23 papers for the non-atomic version).
-
I also don't think we have nailed down an exact semantics of
__verifier_atomic_begin()
so in some sense this is an analysis against an unclear language. (Please correct me if I am wrong here) -
This is also implemented for the
tid
variants of the analyses - is there any consideration for how thread creations and joins interact with this additional atomic notion of protection? -
My biggest concern is
And the unsound combination
mutex-meet-tid-cluster12
with atomics is not available at all.Why exactly is the notion of clusters incompatible with these atomic privatizations? Can similar effects not also arise naturally when the set of protecting mutexes shrinks, causing cluster-like effects to appear on their own? Say, one mutex protecting
{g,h}
and another protecting{h,i}
?
The implementation is more ad-hoc than the conceptual approach I think. Basically
The explicit use of And w.r.t. to stop-the-world or not, that just concerns liveness properties, which is irrelevant for this value analysis.
What do you mean? I think those are orthogonal: unprotected values are still treated the same way by both operations, whether they're associated with
This I don't fully yet understand. Your point about shrinking protection seems like it might be related, especially because this isn't formalized in the papers but just "made to work" in implementations somehow. I suspect this has something to do with not having the set of all global variables (including escaped) at hand. With normal mutexes, we have a set of protected variables and we construct a number of subsets as clusters from it, so a written value goes to all clusters that include the variable. |
Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
Inspired by the Freiburg discussions, it came up that atomic sections are crucial for the validity of their proposed witnesses. We ignore races from atomic sections, but don't use them to privatize values. Here I tried to experiment with that.
Idea
The core idea for making our privatizations do this is straightforward: in an atomic section, a global write should not publish, a global read should read local copy if possible and written globals should only be published once the atomic section ends. Essentially,
unlock(m_g);
s are delayed.Thus, in an atomic section:
lock(m_g); g = x; unlock(m_g);
only doeslock(m_g); g = x;
.lock(m_g); x = g; unlock(m_g);
only doeslock(m_g); x = g;
.__VERIFIER_atomic_end();
doesunlock(m_g);
for allg
whose unlock was delayed. That is all globals that aren't already protected by other mutexes.m_g
is a no-op, because there could be multiplelock(m_g);
s in read/write operations before the atomic section ends.In a way, this adds a meta level to privatizations, where the single atomic meta-mutex protects unprotected writes and delays them, similar to how a normal mutex delays writes.
Implementation
Both implementations pass some test which was previously TODO and a bunch of other tests for soundness that also existed (probably from some earlier naive attempt at atomic privatization).
Base protection
For this I implemented the support just by intuition without considering the more formal description above. So it might still be lacking, especially due to the existing clever implementation tricks.
Relation mutex-meet
I implemented this by quite directly following the formal description above.