ASE 2017

2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2017), October 30 – November 3, 2017, Urbana-Champaign, IL, USA

Desktop Layout

Concurrency
Technical Research
Quick Verification of Concurrent Programs by Iteratively Relaxed Scheduling
Patrick Metzler, Habib Saissi, Péter Bokor, and Neeraj Suri
(TU Darmstadt, Germany)
Preprint
Abstract: The most prominent advantage of software verification over testing is a rigorous check of every possible software behavior. However, large state spaces of concurrent systems, due to non-deterministic scheduling, result in a slow automated verification process. Therefore, verification introduces a large delay between completion and deployment of concurrent software. This paper introduces a novel iterative approach to verification of concurrent programs that drastically reduces this delay. By restricting the execution of concurrent programs to a small set of emph{admissible schedules}, verification complexity and time is drastically reduced. Iteratively adding admissible schedules after their verification eventually restores non-deterministic scheduling. Thereby, our framework allows to find a sweet spot between a low verification delay and sufficient execution time performance. Our evaluation of a prototype implementation on well-known benchmark programs shows that after verifying only few schedules of the program, execution time overhead is competitive to existing deterministic multi-threading frameworks.

Authors:


Time stamp: 2019-06-20T19:28:58+02:00