Relational Mutex-Meet-Privatization making use of Thread IDs

[michael-schwarz]

This is the progress towards realizing the ideas from https://versioncontrolseidl.in.tum.de/schwarz/more-traces.

The implementation deviates from the description in the manuscript in the following way:

• We do not know all initial mutexes and protecting sets a priori, thus we cannot init the local state to set all variables protected by them to their initial values:
  • We always read from an unknown that contains the initial values, unless we know that the corresponding mutex must have been already published to. (amounting to a local write, making that reading superfluous). (LMust set)
• The join of values into local L at thread-join only happens if the thread is unique and must joined. This is a small optimization that preserves soundness but is potentially more precise.
• The handling of single-threaded mode:
  • No publishing of single-threaded values of main thread until we go multithreaded (improving precision)

This subsumes #385, not sure how we want to proceed there?

[sim642]

They do. Not sure why though.

Just had a quick look. They have global variables which are completely unused (OVERFLOW, arr1, arr2). Just removing those makes them more than twice as fast to analyze. Not surprising, since you then have just 6 clusters instead of 21.

[michael-schwarz]

I'd propose we merge this into master now. Any cleanup that I should do before we do?

[sim642]

There are two older comments, which have possibly been buried in the history here:

1. https://github.com/goblint/analyzer/pull/379/files/691be385371d514564d7e3a4c6b56960bef51354..128b1d85e0fdb1d089a73f3f6501e506e0a7339b#diff-58830344d2e5f5b8023333061fe1170c8a94a5e1ba32b98ccf6739eaf20d9123
2. https://github.com/goblint/analyzer/pull/379/files/691be385371d514564d7e3a4c6b56960bef51354..128b1d85e0fdb1d089a73f3f6501e506e0a7339b#diff-f389b2fa9a7f2374023c34533d99d4ed44f8da04d6f46bec9a089ab9ee67b2bd

[michael-schwarz]

The failing indentation seems to be unrelated, as this file was not touched in the PR.
If the changes sufficiently addresses your comments @sim642, I suggest we merge this now.

[sim642]

The failing indentation seems to be unrelated, as this file was not touched in the PR.

I fixed it directly on master, because a change there caused to be already misindented code to appear in unrelated diffs now.