Generalize global constraint variables to module V: Printable.S in each analysis

[sim642]

Closes #469.

Changes

1. Adds module V: Printable.S to each analysis spec, which will be the module used for global constraint variables for that analysis. Since it's abstract V.t can be anything, not necessarily varinfo.
2. Adds 'v type parameter to ctx. This is necessary to make ctx.global and ctx.sideg correctly typed for that V.t.
3. Rewrite MCP's globals handling to use "variants" instead of lists for both global variables and their values. Each variant is just a pair of the analysis ID (int) and the corresponding variable/value as Obj.t.
4. Refactor some analyses to use non-varinfo globals: thread, threadJoins, arinc and extract_arinc.
5. Require analyses to explicitly define V if they want to use any globals (including varinfo). DefaultSpec just uses an empty (variant) type, which means no globals can be used at all.
6. Fix g2html to handle the changed XML where globals have just one analysis value, not all.

TODO

• Comparison runs on sv-benchmarks to see if the abstract variant for globals has any overhead compared to straight varinfo. Also to see if immediately any performance or precision improvement arises from the separation of globals for different analyses.
• Refactor region analysis as well, after removing the dependent shapes analysis (Remove containment, deadlocksByRaces and shapes analyses #474, Remove unmaintained features #460).
• Fix Gobview build.
• Refactor access analysis in Interactive analysis #391 to avoid grouping all struct-based accesses together.

[michael-schwarz]

Looks good thus far! I have to say I am thoroughly impressed that this did not require a major overhaul of everything!

[sim642]

Before (x-axis) and after (y-axis) on SoftwareSystems and ConcurrencySafety:

Disappointingly, the performance only improves in a handful of cases. Also there's no precision improvement (at least on a super high level in the form of better verdicts) on these benchmarks.

I suppose for the single-threaded programs, there shouldn't be a difference anyway because global constraint variables are not used. For multi-threaded programs, I suspect the difference is maybe small because whereever you read a global (from the base analysis variable) the privatization forces the reading of another global (from the mutex analysis variable), so the dependencies we have are still quite tightly coupled between the analyses.

EDIT: I forgot that we now have our benchmarking server publically accessible, so the Benchexec tables are here: https://goblint.cs.ut.ee/results/49-all-fast-gen-glob-after/results/.

[michael-schwarz]

What would be interesting is if the number of globals that are widening points changed, the hypothesis being that less widening might be applied. But then this is super hard to measure because we now have a lot more globals than we did before.

Also, it would be interesting to see what happens with runtime and the number of variables and evaluations if one runs one of the larger multi-threaded programs (e.g. the traces or more traces bechmarks), or some of the other larger projects from our test repo with earlyglobs.

[sim642]

Also, it would be interesting to see what happens with runtime and the number of variables and evaluations if one runs one of the larger multi-threaded programs (e.g. the traces or more traces bechmarks), or some of the other larger projects from our test repo with earlyglobs.

I ran the traces benchmarks before and after, didn't notice much of a difference there either (and the bigger programs were from sv-benchmarks anyway). I don't know about the single-threaded benchmarks in bench though.

It's also the case that the base analysis and privatizations still use varinfo variables for everything. I don't know yet if there are any real opportunities to use the new generalization there, because most of the additional global variable components (background lockset, write lockset, thread ID) still need to be universally quantified over, so the (nested) maps need to remain to make that possible.

[sim642]

It's also the case that the base analysis and privatizations still use varinfo variables for everything. I don't know yet if there are any real opportunities to use the new generalization there, because most of the additional global variable components (background lockset, write lockset, thread ID) still need to be universally quantified over, so the (nested) maps need to remain to make that possible.

I have now also refactored all the privatizations at the top level at least. So no more MUTEX_GLOBAL_g and MUTEX_INITS varinfos any more. Similarly for base protection-based I separated the unprotected and protected globals (which as discussed on Slack can make thing non-terminatingly more precise). For per-mutex privatizations this generalization also allows the privatization to account for mutex offsets, which were previously just stripped for privatization, although the protecting locksets could have them.

Moreover, I replaced the global product domains for those things with Lift2s.

EDIT: I now went even further and also made the base analysis globals a variant of the privatization's globals or thread returns. This allowed getting rid of all the thread return handling that previously had to be in all the privatizations because they were completely in charge of base's globals. Also it allowed to get rid of to_varinfo etc on thread IDs altogether because they're now first-class citizens everywhere!

[sim642]

I ran sv-benchmarks again after my futher refactorings and there is now a 3% improvement in the regression line compared to master:

(Full comparisons here: https://goblint.cs.ut.ee/results/50-all-fast-gen-glob-after-refactor/results/).

I'm not sure where this improvement exactly came from though because the changes were to privatizations, which only matter for concurrent benchmarks and even then we don't use any of the more expensive privatizations.