uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Programming Languages)
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Programming Languages)ORCID iD: 0000-0001-9657-0179
2017 (English)In: Journal of the ACM, ISSN 0004-5411, E-ISSN 1557-735X, Vol. 64, no 4, article id 25Article in journal (Refereed) Published
Abstract [en]

Stateless model checking is a powerful method for program verification that, however, suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, is Dynamic Partial Order Reduction (DPOR), an algorithm originally introduced by Flanagan and Godefroid in 2005 and since then not only used as a point of reference but also extended by various researchers. In this article, we present a new DPOR algorithm, which is the first to be provably optimal in that it always explores the minimal number of executions. It is based on a novel class of sets, called source sets, that replace the role of persistent sets in previous algorithms. We begin by showing how to modify the original DPOR algorithm to work with source sets, resulting in an efficient and simple-to-implement algorithm, called source-DPOR. Subsequently, we enhance this algorithm with a novel mechanism, called wakeup trees, that allows the resulting algorithm, called optimal-DPOR, to achieve optimality. Both algorithms are then extended to computational models where processes may disable each other, for example, via locks. Finally, we discuss tradeoffs of the source-and optimal-DPOR algorithm and present programs that illustrate significant time and space performance differences between them. We have implemented both algorithms in a publicly available stateless model checking tool for Erlang programs, while the source-DPOR algorithm is at the core of a publicly available stateless model checking tool for C/pthread programs running on machines with relaxed memory models. Experiments show that source sets significantly increase the performance of stateless model checking compared to using the original DPOR algorithm and that wakeup trees incur only a small overhead in both time and space in practice.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2017. Vol. 64, no 4, article id 25
National Category
Software Engineering
Identifiers
URN: urn:nbn:se:uu:diva-331842DOI: 10.1145/3073408ISI: 000410615900002OAI: oai:DiVA.org:uu-331842DiVA, id: diva2:1150369
Projects
UPMARCRELEASE
Funder
EU, FP7, Seventh Framework Programme, 287510Swedish Research CouncilAvailable from: 2017-10-18 Created: 2017-10-18 Last updated: 2018-01-13Bibliographically approved
In thesis
1. Effective Techniques for Stateless Model Checking
Open this publication in new window or tab >>Effective Techniques for Stateless Model Checking
2018 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

Stateless model checking is a technique for testing and verifying concurrent programs, based on exploring the different ways in which operations executed by the processes of a concurrent program can be scheduled. The goal of the technique is to expose all behaviours that can be a result of scheduling non-determinism. As the number of possible schedulings is huge, however, techniques that reduce the number of schedulings that must be explored to achieve verification have been developed. Dynamic partial order reduction (DPOR) is a prominent such technique.

This dissertation presents a number of improvements to dynamic partial order reduction that significantly increase the effectiveness of stateless model checking. Central among these improvements are the Source and Optimal DPOR algorithms (and the theoretical framework behind them) and a technique that allows the observability of the interference of operations to be used in dynamic partial order reduction. Each of these techniques can exponentially decrease the number of schedulings that need to be explored to verify a concurrent program. The dissertation also presents a simple bounding technique that is compatible with DPOR algorithms and effective for finding bugs in concurrent programs, if the number of schedulings is too big to make full verification possible in a reasonable amount of time, even when the improved algorithms are used.

All improvements have been implemented in Concuerror, a tool for applying stateless model checking to Erlang programs. In order to increase the effectiveness of the tool, the interference of the high-level operations of the Erlang/OTP implementation is examined, classified and precisely characterized. Aspects of the implementation of the tool are also described. Finally, a use case is presented, showing how Concuerror was used to find bugs and verify key correctness properties in repair techniques for the CORFU chain replication protocol.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2018. p. 56
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1602
Keywords
Concurrent, Parallel, Model Checking, Partial Order Reduction, Dynamic Partial Order Reduction, DPOR, Sleep Set Blocking, Source Sets, Source DPOR, Wakeup Trees, Optimal DPOR, Observers, Verification, Bounding, Exploration Tree Bounding, Testing, Erlang, Concuerror, Protocol, Chain Replication, CORFU
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-333541 (URN)978-91-513-0160-0 (ISBN)
Public defence
2018-02-02, ITC/2446, Lägerhyddsvägen 2, 752 37, Uppsala, 13:15 (English)
Opponent
Supervisors
Projects
UPMARCRELEASE
Available from: 2017-12-19 Created: 2017-11-22 Last updated: 2018-03-08

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records BETA

Abdulla, ParoshAronis, StavrosJonsson, BengtSagonas, Konstantinos

Search in DiVA

By author/editor
Abdulla, ParoshAronis, StavrosJonsson, BengtSagonas, Konstantinos
By organisation
Computer SystemsComputing Science
In the same journal
Journal of the ACM
Software Engineering

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 237 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf