Incremental benchmarking script and suite

[vesalvojdani]

This is a hacky first version of a script that does more or less what I want. The final version will be just as hacky, but it should also allow all these different flags to be compared and maybe integrate the precision comparison from the other script. The critical thing at this stage is to have some way to sanity check performance issues to determine the viability of this approach.

Still a few things to do here:

• Fix it to work on non-kernel benchmarks.
• Update the readme with the instructions that I had dumped here.
• Set the proper parameters for the interactive branch
• Incorporate the precision comparison.
• Finalize the initial benchmark suite.

Some post-finalization steps:

• Display if incremental has something that is incomparable, more precise, or less.
• Add some restart-needing examples in separate directory.
• Run this stupid thing with intervals...
• Try to add some diffs to previous benchmarks that need a restart.

[vesalvojdani]

So there's not really a need to "review" this, but I wanted to add some explanation of how to use it somewhere. I will maybe move this into the readme file for this repo. Might be good to have some more explanations of what all the different things are in this repo. But there are many scripts here, and I don't know what half of them are for... :)

[vogler]

I'm using the following:

• parallel-run.sh to run the config in that script in parallel and log each program
• csv-results.ml to extract some numbers from each log and print a csv of it
• precision.sh to let goblint compare two variants for each program and write the result to a .precision file

The other (old) scripts can probably be removed.

Copying the csv to LibreOffice to get some ratios/graphs is a bit annoying, but not sure if it's worth generating something since it depends on the benchmark.

[vesalvojdani]

We can let the renaming ids serve as baseline. It makes no significant difference to the run time. Something is very fishy with my comparison script or with the benchmarks because currently it seems to imply that we compute exactly the same values even without restart: results. At least, I thought this patch would result in a change in protected mutexes for a specific global. I will have to look into this.

[vesalvojdani]

It seems that the script and compare operations are actually working. It does report on example I added. These patches are fairly small... Might need to look at some sort of mutex-based simple example to be sure it really is working. The above patch results in variables like (struct findserv_req).sin.sin_port to becoming safe, but these are our type-based hacks that are not used for privatization, so that might explain why nothing gets refined here.

[sim642]

Also goblint/analyzer#397 is not yet in Goblint's interactive branch, so races (or the lack thereof) has nothing to do with anything in the solution or restarting.

It should still matter for protecting locksets, but if there still are other unprotected accesses, then the protecting lockset in the global invariant cannot improve either.

[vesalvojdani]

Okay, running with intervals enable doesn't change the story much: results. There was an incomparable thing before as well, but now there is a verification failure with Difference: Dead code instead of bot...

[vesalvojdani]

This is now a fairly good initial benchmark set. With Interval analysis turned on there are examples where precision is lost without restarting, but right now too much gets restarted. It is very fishy because even diffs that should not change anything globally results in restarts. Also, earlyglobs does not help.