Add some hacky atomic privatizations

[sim642]

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:

1. lock(m_g); g = x; unlock(m_g); only does lock(m_g); g = x;.
2. lock(m_g); x = g; unlock(m_g); only does lock(m_g); x = g;.
3. __VERIFIER_atomic_end(); does unlock(m_g); for all g whose unlock was delayed. That is all globals that aren't already protected by other mutexes.
4. Ensure that recursive locking of m_g is a no-op, because there could be multiple lock(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.

[michael-schwarz]

I have not looked at the implementation yet, but starting from the formal description, I started wondering for the relational privatization:

• If not performing any unlock but doing lock repeatedly might be a problem, as the value stored at m_g might be outdated and yield bot when meeting the local state with it. This is adressed by (4) above.
• if the same situation can arise because of other mutexes that are acquired inside the atomic block and that disagree with the local state. It seems that this cannot be the case, as any such mutex is either (a) not protecting or (b) has been locked and unlocked when writing.
• Are unlocks for m_g also delayed for globals that are protected? If yes, it seems like it would still be necessary to publish their values at the end of the atomic section...

[sim642]

• Are unlocks for m_g also delayed for globals that are protected? If yes, it seems like it would still be necessary to publish their values at the end of the atomic section...

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.

[michael-schwarz]

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?

[sim642]

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.

[sim642]

Another interesting observation is that the Freiburg case_distinction example could be handled directly with relational analysis, but it requires the relational domain to support disjunction (a la the outdated bddapron or by lifting our relation analysis to a set of abstract states). The second missing component is unprotected relational invariants which in the presence of these atomic sections updating multiple globals become more interesting. Ghost variables then introduce case splitting purely within the relational abstract domain.

[sim642]

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 mutex-meet-tid-cluster12 with atomics is not available at all.

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.

[michael-schwarz]

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}?

[sim642]

• 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).

The implementation is more ad-hoc than the conceptual approach I think. Basically __VERIFIER_atomic protects all global accesses instead of per-global $m_g$-s. It's just coarser and has worse dependency structure, but has all the same unprotected thread interactions. In terms of formalization, this shouldn't make a difference in the general mutex handling. It's just a technical assumption that $m_g$-s (or __VERIFIER_atomic) is locked and unlocked around all accesses. All this does is not unlock and relock __VERIFIER_atomic between global accesses within an explicit section. And all that does is that the intermediate state isn't exposed to anyone (even without protection).

• 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)

The explicit use of __VERIFIER_atomic_begin in simple cases like what's handled here isn't the problematic part I think. In the Freiburg collaboration, the issues arise from how these atomic blocks automatically get induced from ghost assignments and where and when this should be allowed. Here the programs already specify atomic blocks themselves, so nothing is being made atomic that the program itself already doesn't want.

And w.r.t. to stop-the-world or not, that just concerns liveness properties, which is irrelevant for this value analysis.

• 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?

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 $m_g$ or __VERIFIER_atomic.

• 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}?

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.
With unprotected writes, we cannot list all the superset clusters a variable could be in, so a write isn't added to all the clusters that will ever occur. In some sense, when reading, one has to consider the join of all unprotected clusters, not the meet. Or I guess equivalently, just collapse the unprotected invariant into a single cluster, like we do with initializers I think.