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
Effective Techniques for Stateless Model Checking
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computing Science. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (Programming Languages)
2018 (English)Doctoral thesis, comprehensive summary (Other academic)
Description
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. , 56 p.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1602
Keyword [en]
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: urn:nbn:se:uu:diva-333541ISBN: 978-91-513-0160-0 (print)OAI: oai:DiVA.org:uu-333541DiVA: diva2:1159517
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-01-13
List of papers
1. Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction
Open this publication in new window or tab >>Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction
2017 (English)In: Journal of the ACM, ISSN 0004-5411, E-ISSN 1557-735X, Vol. 64, no 4, 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
National Category
Software Engineering
Identifiers
urn:nbn:se:uu:diva-331842 (URN)10.1145/3073408 (DOI)000410615900002 ()
Projects
UPMARCRELEASE
Funder
EU, FP7, Seventh Framework Programme, 287510Swedish Research Council
Available from: 2017-10-18 Created: 2017-10-18 Last updated: 2018-01-13Bibliographically approved
2. The shared-memory interferences of Erlang/OTP built-ins
Open this publication in new window or tab >>The shared-memory interferences of Erlang/OTP built-ins
2017 (English)In: Proceedings of the 16th ACM SIGPLAN International Workshop on Erlang, New York: Association for Computing Machinery (ACM), 2017Conference paper, Published paper (Refereed)
Abstract [en]

Erlang is a concurrent functional language based on the actor modelof concurrency. In the purest form of this model, actors are realizedby processes that do not share memory and communicate witheach other exclusively via message passing. Erlang comes quiteclose to this model, as message passing is the primary form of interprocesscommunication and each process has its own memoryarea that is managed by the process itself. For this reason, Erlangis often referred to as implementing “shared nothing” concurrency.Although this is a convenient abstraction, in reality Erlang’s mainimplementation, the Erlang/OTP system, comes with a large numberof built-in operations that access memory which is shared byprocesses. In this paper, we categorize these built-ins, and characterizethe interferences between them that can result in observabledifferences of program behaviour when these built-ins are usedin a concurrent setting. The paper is complemented by a publiclyavailable suite of more than one hundred small Erlang programsthat demonstrate the racing behaviour of these built-ins.

Place, publisher, year, edition, pages
New York: Association for Computing Machinery (ACM), 2017
Keyword
Actors, BEAM, Concuerror, Erlang, Scheduling nondeterminism
National Category
Software Engineering
Identifiers
urn:nbn:se:uu:diva-331840 (URN)10.1145/3123569.3123573 (DOI)978-1-4503-5179-9 (ISBN)
Conference
ERLANG 2017
Projects
UPMARC
Available from: 2017-10-18 Created: 2017-10-18 Last updated: 2018-01-13Bibliographically approved
3. Testing And Verifying Chain Repair Methods For CORFU Using Stateless Model Checking
Open this publication in new window or tab >>Testing And Verifying Chain Repair Methods For CORFU Using Stateless Model Checking
2017 (English)Conference paper, Published paper (Refereed)
Abstract [en]

Corfu is a distributed shared log that is designed to be scalable and reliable in the presence of failures and asynchrony. Internally, Corfu is fully replicated for fault tolerance, without sharding data or sacrificing strong consistency. In this case study, we present the modeling approaches we followed to test and verify, using Concuerror, the correctness of repair methods for the Chain Replication protocol suitable for Corfu. In the first two methods we tried, Concuerror located bugs quite fast. In contrast, the tool did not manage to find bugs in the third method, but the time this took also motivated an improvement in the tool that reduces the number of traces explored. Besides more details about all the above, we present experiences and lessons learned from applying stateless model checking for verifying complex protocols suitable for distributed programming.

Place, publisher, year, edition, pages
Cham: Springer, 2017
Series
Lecture Notes in Computer Science, 10510
National Category
Computer Systems Software Engineering
Identifiers
urn:nbn:se:uu:diva-331836 (URN)10.1007/978-3-319-66845-1_15 (DOI)978-3-319-66844-4 (ISBN)978-3-319-66845-1 (ISBN)
Conference
Integrated Formal Methods. IFM 2017
Projects
UPMARC
Available from: 2017-10-18 Created: 2017-10-18 Last updated: 2018-01-13Bibliographically approved
4. Optimal Dynamic Partial Order Reduction with Observers
Open this publication in new window or tab >>Optimal Dynamic Partial Order Reduction with Observers
(English)Manuscript (preprint) (Other academic)
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-333508 (URN)
Projects
UPMARC
Available from: 2017-11-21 Created: 2017-11-21 Last updated: 2018-01-13

Open Access in DiVA

fulltext(634 kB)49 downloads
File information
File name FULLTEXT01.pdfFile size 634 kBChecksum SHA-512
9cb432872b732dea37d238085d085019cb0207430674fc1787350258b14f75b0cf03b6fa7740b4b76154f85381235e8ab67f4b637d8426a425a20e3015888fcb
Type fulltextMimetype application/pdf

Authority records BETA

Aronis, Stavros

Search in DiVA

By author/editor
Aronis, Stavros
By organisation
Division of Computing ScienceComputing Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 49 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

isbn
urn-nbn

Altmetric score

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