Optimize `none` base privatization, add eager Vojdani privatization

[sim642]

none privatizations

The none privatization in base analysis is a sliced copy of the old unsound Vojdani privatization (which was removed in #736). Thus, it is still based on sync: write_global doesn't side-effect, but adds to local state and sync does all the side effects. This is an unnecessarily roundabout way to be (almost) as imprecise as possible. What's perhaps worse is that it syncs unconditionally (so not just at join points) and each time iterates over the entire cpa. This could be a stupid hidden cost when wanting super-fast analysis without any privatization, e.g. our large-program example conf. This is quadratically bad in program size (nodes * variables) compared to protection privatization almost none of this would happen.

In this PR, I've added NonePriv2, which doesn't rely on sync (except for the inevitable branched thread creation) and surprisingly fails fewer tests when made the default privatization on our regression suite (it's more precise or more sound?!). It's constructed according to some old traces related work and still has global variables in local states (but reads them joined with global unknowns).

Finally, I've added NonePriv3, which never puts any globals into local states (in multi-threaded mode), and has read_global and write_global directly using getg and sideg, respectively. This is what probably should just replace NonePriv, but I've added them all right now to make investigating differences and benchmarking slightly easier.

EDIT: Now only NonePriv3 remains in place of NonePriv.

Eager Vojdani privatization

#736 removed the old unsound Vojdani privatization which triggered the whole traces research direction. Its unsoundness was due to an attempt at lazy reading (which was only hinted at in some thesis/paper but I cannot find anymore where).

In this PR, I've added VojdaniPriv, which is the sound Vojdani privatization as described in his thesis and various papers. This does eager reading, which should avoid the unsoundness. It also doesn't use sync because it handles lock and unlock itself, but that may also be a mistake when trying to represent the original analysis faithfully.

I don't know if we'd want to have this back, but it could also make for interesting benchmarking.

[sim642]

I don't know if we'd want to have this back, but it could also make for interesting benchmarking.

And indeed it did, on SV-COMP ConcurrencySafety at least (if I implemented everything correctly):

• vojdani with its eagerness is slower than the others most of the way, which is expected. However, at the high end it's faster than protection.
• vojdani is also more precise than protection on many tasks. Only protection-read makes it more precise than vojdani again.
• protection-read (and by a tiny margin protection) are faster than any of the none variants, which is quite surprising. I suppose this is due to a fewer side effects and such dependencies, but it could mean that our large-program example conf is recommending a less precise and slower analysis than out of the box.

[michael-schwarz]

I will hopefully get around to reviewing this within the next week or so!