uu.seUppsala universitets publikasjoner
Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Optimal dynamic partial order reduction with observers
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi. (Programming Languages)
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi. (Programming Languages)ORCID-id: 0000-0001-9657-0179
2018 (engelsk)Inngår i: Tools and Algorithms for the Construction and Analysis of Systems: Part II, Springer, 2018, Vol. 10806, s. 229-248Konferansepaper, Publicerat paper (Fagfellevurdert)
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.

sted, utgiver, år, opplag, sider
Springer, 2018. Vol. 10806, s. 229-248
Serie
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 10806
HSV kategori
Identifikatorer
URN: urn:nbn:se:uu:diva-333508DOI: 10.1007/978-3-319-89963-3 _ 14ISI: 000445822600014ISBN: 978-3-319-89962-6 (tryckt)ISBN: 978-3-319-89963-3 (digital)OAI: oai:DiVA.org:uu-333508DiVA, id: diva2:1159055
Konferanse
TACAS 2018, April 14–20, Thessaloniki, Greece.
Prosjekter
UPMARC
Forskningsfinansiär
Swedish Research CouncilTilgjengelig fra: 2018-04-14 Laget: 2017-11-21 Sist oppdatert: 2019-01-07bibliografisk kontrollert
Inngår i avhandling
1. Effective Techniques for Stateless Model Checking
Åpne denne publikasjonen i ny fane eller vindu >>Effective Techniques for Stateless Model Checking
2018 (engelsk)Doktoravhandling, med artikler (Annet vitenskapelig)
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.

sted, utgiver, år, opplag, sider
Uppsala: Acta Universitatis Upsaliensis, 2018. s. 56
Serie
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1602
Emneord
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
HSV kategori
Forskningsprogram
Datavetenskap
Identifikatorer
urn:nbn:se:uu:diva-333541 (URN)978-91-513-0160-0 (ISBN)
Disputas
2018-02-02, ITC/2446, Lägerhyddsvägen 2, 752 37, Uppsala, 13:15 (engelsk)
Opponent
Veileder
Prosjekter
UPMARCRELEASE
Tilgjengelig fra: 2017-12-19 Laget: 2017-11-22 Sist oppdatert: 2018-03-08

Open Access i DiVA

fulltext(19127 kB)171 nedlastinger
Filinformasjon
Fil FULLTEXT01.pdfFilstørrelse 19127 kBChecksum SHA-512
7139b0a0f4424d652f42f76456a7a225fabf21963df1158863ff50698ee85b55ab903889b32e8e99a4d9e614caddfa1188bd0170f1819a0248058f5e262dc629
Type fulltextMimetype application/pdf

Andre lenker

Forlagets fulltekstFörlagets fulltext - Bok

Personposter BETA

Aronis, StavrosJonsson, BengtSagonas, Konstantinos

Søk i DiVA

Av forfatter/redaktør
Aronis, StavrosJonsson, BengtLång, MagnusSagonas, Konstantinos
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar
Totalt: 171 nedlastinger
Antall nedlastinger er summen av alle nedlastinger av alle fulltekster. Det kan for eksempel være tidligere versjoner som er ikke lenger tilgjengelige

doi
isbn
urn-nbn

Altmetric

doi
isbn
urn-nbn
Totalt: 518 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf