Skip to content
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

Optimize none base privatization, add eager Vojdani privatization #1552

Open
wants to merge 10 commits into
base: master
Choose a base branch
from

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Aug 2, 2024

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 sim642 added performance Analysis time, memory usage benchmarking labels Aug 2, 2024
@sim642
Copy link
Member Author

sim642 commented Aug 5, 2024

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.

image

@sim642 sim642 marked this pull request as ready for review October 25, 2024 12:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
benchmarking performance Analysis time, memory usage
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant