Parallel bug-finding in concurrent programs via reduced interleaving instances

Nguyen, Truc L, Schrammel, Peter, Fischer, Bernd, La Torre, Salvatore and Parlato, Gennaro (2017) Parallel bug-finding in concurrent programs via reduced interleaving instances. The 32nd IEEE/ACM International Conference on Automated Software Engineering, University of Illinois, 30th October - 3rd November. Published in: Automated Software Engineering. ACM ISSN 0928-8910 (Accepted)

[img] PDF - Accepted Version
Restricted to SRO admin only

Download (297kB)

Abstract

Concurrency poses a major challenge for program verification, but it can also offer an opportunity to scale when subproblems can be analysed in parallel. We exploit this opportunity here and use a parametrizable code-to-code translation to generate a set of simpler program instances, each capturing a reduced set of the original program’s interleavings. These instances can then be checked independently in parallel. Our approach does not depend on the tool that is chosen for the final analysis, is compatible with weak memory models, and amplifies the effectiveness of existing tools, making them find bugs faster and with fewer resources. We use Lazy-CSeq as an off-the-shelf final verifier to demonstrate that our approach is able, already with a small number of cores, to find bugs in the hardest known concurrency benchmarks in a matter of minutes, whereas other dynamic and static tools fail to do so in hours.

Item Type: Conference Proceedings
Keywords: verification, concurrency, sequentialisation, parallelisation
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Q Science > QA Mathematics > QA0076 Computer software
Depositing User: Peter Schrammel
Date Deposited: 14 Sep 2017 08:20
Last Modified: 30 Oct 2017 10:57
URI: http://sro.sussex.ac.uk/id/eprint/70188

View download statistics for this item

📧 Request an update