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
Optimal dynamic partial order reduction with observers
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, Computer Systems.
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)ORCID iD: 0000-0001-9657-0179
2018 (English)In: Tools and Algorithms for the Construction and Analysis of Systems: Part II, Springer, 2018, Vol. 10806, p. 229-248Conference paper, Published paper (Refereed)
Abstract [en]

Dynamic partial order reduction (DPOR) algorithms are used in stateless model checking (SMC) to combat the combinatorial explosion in the number of schedulings that need to be explored to guarantee soundness. The most effective of them, the Optimal DPOR algorithm, is optimal in the sense that it explores only one scheduling per Mazurkiewicz trace. In this paper, we enhance DPOR with the notion of observability, which makes dependencies between operations conditional on the existence of future operations, called observers. Observers naturally lead to a lazy construction of dependencies. This requires significant changes in the core of POR algorithms (and Optimal DPOR in particular), but also makes the resulting algorithm, Optimal DPOR with Observers, super-optimal in the sense that it explores exponentially less schedulings than Mazurkiewicz traces in some cases. We argue that observers come naturally in many concurrency models, and demonstrate the performance benefits that Optimal DPOR with Observers achieves in both an SMC tool for shared memory concurrency and a tool for concurrency via message passing, using both synthetic and actual programs as benchmarks.

Place, publisher, year, edition, pages
Springer, 2018. Vol. 10806, p. 229-248
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 10806
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-333508DOI: 10.1007/978-3-319-89963-3 _ 14ISI: 000445822600014ISBN: 978-3-319-89962-6 (print)ISBN: 978-3-319-89963-3 (electronic)OAI: oai:DiVA.org:uu-333508DiVA, id: diva2:1159055
Conference
TACAS 2018, April 14–20, Thessaloniki, Greece.
Projects
UPMARC
Funder
Swedish Research CouncilAvailable from: 2018-04-14 Created: 2017-11-21 Last updated: 2019-01-07Bibliographically 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

fulltext(19127 kB)151 downloads
File information
File name FULLTEXT01.pdfFile size 19127 kBChecksum SHA-512
7139b0a0f4424d652f42f76456a7a225fabf21963df1158863ff50698ee85b55ab903889b32e8e99a4d9e614caddfa1188bd0170f1819a0248058f5e262dc629
Type fulltextMimetype application/pdf

Other links

Publisher's full textFörlagets fulltext - Bok

Authority records BETA

Aronis, StavrosJonsson, BengtSagonas, Konstantinos

Search in DiVA

By author/editor
Aronis, StavrosJonsson, BengtLång, MagnusSagonas, Konstantinos
By organisation
Computing ScienceComputer Systems
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 151 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 487 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