Claim I: Sequential vs. Parallel Algorithm
The following quantile plots show the results of BAM with value analysis, sequential version compared to parallel version with one thread.
A preprint of this article is available for you to download. The published paper is available from ACM.
The approach was presented at ASE 2018 (slides) and CPA 2018 (slides).
Recent development of software aims at massively parallel execution, because of the trend to increase the number of processing units per CPU socket. But many approaches for program analysis are not designed to benefit from a multi-threaded execution and lack support to utilize multi-core computers. Rewriting existing algorithms is difficult and error-prone, and the design of new parallel algorithms also has limitations. An orthogonal problem is the granularity: computing each successor state in parallel seems too fine-grained, so the open question is to find the right structural level for parallel execution. We propose an elegant solution to these problems: Block summaries should be computed in parallel. Many successful approaches to software verification are based on summaries of control-flow blocks, large blocks, or function bodies. Block-abstraction memoization is a successful domain-independent approach for summary-based program analysis. We redesigned the verification approach of block-abstraction memoization starting from its original recursive definition, such that it can run in a parallel manner for utilizing the available computation resources without losing its advantages of being independent from a certain abstract domain. We present an implementation of our new approach for multi-core shared-memory machines. The experimental evaluation shows that our summary-based approach has no significant overhead compared to the existing sequential approach and that it has a significant speedup when using multi-threading.
The supplementary archive contains all data, tables, used benchmark programs, and configurations as well as a ready-to-run version of CPAchecker. Next to a README, the supplementary archive contains the tool CPAchecker ./CPAchecker/ and our experimental results ./results-VABAM-VAparallelBAM/ ./results-VAparallelBAM/ .
./CPAchecker/The CPAchecker configuration files that we used in the experiments.
./benchmark-definitions/The input files for our benchmarking script. They depend on programs from the SV-Benchmark repository.
./results-VABAM-VAparallelBAM/Our raw results for the comparison of plain Value Analysis, BAM with Value Analysis, and our new parallel approach, including log files (see also below).
./results-VAparallelBAM/Our raw results for the comparison of our new parallel approach with different numbers of CPU cores, including log files (see also below).
./tables/Our raw tables (see also below).
The rest of the files are part of a ready-to-run version of CPAchecker, revision 28809.
The results of the evaluation in the paper are available here:
You can click on the cells in the status columns in these tables to see the output of the corresponding tool. Clicking on the column headings (e.g., “cputime”) will produce a plot with the quantile function of the values of this column. This requires JavaScript in your browser.
In order to reproduce the results, download the supplementary archive (that includes CPAchecker). Our benchmark script assumes the extracted archives for all tools in the same directory than our extracted archive. The evaluation was done on an Ubuntu 16.04 (64 bit).
scripts/benchmark.py ../benchmark-definitions/bam-parallel.xml