Distributed Summary Synthesis
This work is accepted at FSE 2024. A preprint and the publisher's version of this article are available for you to download.
Abstract
There are many approaches for automated software verification, but they are either imprecise, do not scale well to large systems, or do not sufficiently leverage parallelization. This hinders the integration of software model checking into the development process (continuous integration). We propose an approach to decompose one large verification task into multiple smaller, connected verification tasks, based on blocks in the program control flow. For each block, summaries are computed - based on independent, distributed, continuous refinement by communication via messages between the blocks. The approach iteratively synthesizes preconditions to assume at the block entry (which program states reach this block) and verification conditions to check at the block exit (which program states lead to a specification violation). This separation of concerns leads to an architecture in which all blocks can be analyzed in parallel, as independent verification problems. Whenever new information (as a precondition or verification condition) is available from other blocks, the verification can decide to restart with this new information. We realize our approach as an extension of the configurable-program-analysis algorithm and implement it for the verification of C programs in the widely used verifier CPAchecker. A large experimental evaluation shows the potential of our new approach: The distribution of the workload to several processing units works well and there is a significant reduction of the response time when using multiple processing units. There are even cases in which the new approach beats the highly-tuned, existing single-threaded predicate abstraction.
Tool and Reproduction Information
A reproduction package of this work is available on Zenodo (). The implementation of DSS in CPAchecker can be found in our SVN repository.
Full Results
The experimental results reported in the paper can be seen in the interactive tables below. You can click on the cells in the status columns to see the corresponding log output and use the respective tabs to show various plots.
- RQ1: Distribution of Workload
- RQ2: Reduction of response time
- RQ3: Outperform Predicate Abstraction on some Tasks
- RQ4: Complement State of the Art
- RQ5: Parallel Portfolio
Task | $\mathrm{CPU}{\mathbb{}}_{P}$ | $\mathrm{CPU}{\mathbb{}}_{\mathrm{DSS}}$ | $\mathrm{RT}{\mathbb{}}_{P}$ | $\mathrm{RT}{\mathbb{}}_{\mathrm{DSS}}$ | $\mathrm{num.\; threads}$ | $\mathrm{avg.\; block\; size}$ |
---|---|---|---|---|---|---|
leds--leds-regulator... | 44.76 s | 33.23 s | 30.83 s | 7.18 s | 92 | 12.40 |
rtc--rtc-ds1553.ko-l... | 49.04 s | 64.55 s | 30.33 s | 13.98 s | 164 | 14.98 |
rtc--rtc-stk17ta8.ko... | 46.72 s | 67.87 s | 28.93 s | 15.11 s | 162 | 15.70 |
watchdog--it8712f_w... | 86.78 s | 50.26 s | 68.99 s | 15.89 s | 216 | 7.91 |
ldv-commit-tester/m0... | 50.10 s | 102.93 s | 28.81 s | 20.99 s | 230 | 7.00 |
Technique | Correctly solved | Timeout | Out of memory | Error |
---|---|---|---|---|
k-Induction | 985 | 450 | 28 | 1022 |
Predicate | 860 | 696 | 14 | 915 |
IMC | 707 | 24 | 15 | 1739 |
DSS | 592 | 264 | 1117 | 512 |