swarm-ASE2017.pdf (290.06 kB)
Parallel bug-finding in concurrent programs via reduced interleaving instances
conference contribution
posted on 2023-06-09, 07:54 authored by Truc L Nguyen, Peter Schrammel, Bernd Fischer, Salvatore La Torre, Gennaro ParlatoConcurrency 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.
History
Publication status
- Published
File Version
- Accepted version
Journal
Automated Software EngineeringISSN
0928-8910Publisher
Association for Computing MachineryPublisher URL
Page range
753-764Event name
The 32nd IEEE/ACM International Conference on Automated Software EngineeringEvent location
University of IllinoisEvent type
conferenceEvent date
30th October - 3rd NovemberISBN
9781538626849Department affiliated with
- Informatics Publications
Full text available
- Yes
Peer reviewed?
- Yes
Legacy Posted Date
2017-09-14First Open Access (FOA) Date
2018-05-31First Compliant Deposit (FCD) Date
2017-09-13Usage metrics
Categories
No categories selectedLicence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC