Extracting safe thread schedules from incomplete model checking results
- PDF / 1,084,449 Bytes
- 17 Pages / 595.276 x 790.866 pts Page_size
- 46 Downloads / 214 Views
STTT Special Issue: SPIN 2019
Extracting safe thread schedules from incomplete model checking results Patrick Metzler1 · Neeraj Suri2 · Georg Weissenbacher3
© The Author(s) 2020
Abstract Model checkers frequently fail to completely verify a concurrent program, even if partial-order reduction is applied. The verification engineer is left in doubt whether the program is safe and the effort toward verifying the program is wasted. We present a technique that uses the results of such incomplete verification attempts to construct a (fair) scheduler that allows the safe execution of the partially verified concurrent program. This scheduler restricts the execution to schedules that have been proven safe (and prevents executions that were found to be erroneous). We evaluate the performance of our technique and show how it can be improved using partial-order reduction. While constraining the scheduler results in a considerable performance penalty in general, we show that in some cases our approach—somewhat surprisingly—even leads to faster executions. Keywords Software verification · Model checking · Concurrency · Nondeterministic scheduling
1 Introduction Automated verification of concurrent programs is inherently difficult because of exponentially large state spaces [41]. State space reductions such as partial-order reduction (POR) [10,16,17] allow a model checker to focus on a subset of all reachable states, while the verification result is valid for all reachable states. However, even reduced state spaces may be P. Metzler was supported by the German Academic Exchange Service (DAAD). N. Suri was supported in part by H2020-SU-ICT-2018-2 CONCORDIA GA #830927 and BMBF-Hessen TUD CRISP. G. Weissenbacher was funded by the Vienna Science and Technology Fund (WWTF) through the project Heisenbugs (VRG11-005) and the LogiCS doctoral program W1255-N23 of the Austrian Science Fund (FWF).
B
Patrick Metzler [email protected] Neeraj Suri [email protected] Georg Weissenbacher [email protected]
1
TU Darmstadt, Darmstadt, Germany
2
Lancaster University, Bailrigg, UK
3
TU Wien, Vienna, Austria
intractably large [17] and corresponding programs infeasible to (automatically) verify, requiring manual intervention. We propose a novel model checking approach for safety verification of potentially nonterminating programs with a bounded number of threads, nondeterministic scheduling, and shared memory. Our approach iteratively generates incomplete verification results (IVRs) to prove the safety of a program under a (semi-)deterministic scheduler. Our contribution is the novel generation and use of IVRs based on existing model checking algorithms, where we use lazy abstraction with interpolants [42] to instantiate our approach. The scheduling constraints induced by an IVR can be enforced by iteratively relaxed scheduling [29], a technique to enforce fine-grained orderings of concurrent memory events. When the scheduling constraints of an IVR are enforced, all executions (for all possible inputs) are s
Data Loading...
