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
Testing And Verifying Chain Repair Methods For CORFU Using Stateless Model Checking
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, Datalogi. (Programming Languages)ORCID-id: 0000-0001-9657-0179
VMware, Cambridge, MA, USA.
2017 (engelsk)Konferansepaper, Publicerat paper (Fagfellevurdert)
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.

sted, utgiver, år, opplag, sider
Cham: Springer, 2017. s. 227-242
Serie
Lecture Notes in Computer Science ; 10510
HSV kategori
Identifikatorer
URN: urn:nbn:se:uu:diva-331836DOI: 10.1007/978-3-319-66845-1_15ISBN: 978-3-319-66844-4 (tryckt)ISBN: 978-3-319-66845-1 (digital)OAI: oai:DiVA.org:uu-331836DiVA, id: diva2:1150359
Konferanse
Integrated Formal Methods. IFM 2017
Prosjekter
UPMARCTilgjengelig fra: 2017-10-18 Laget: 2017-10-18 Sist oppdatert: 2018-01-13bibliografisk 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(196 kB)128 nedlastinger
Filinformasjon
Fil FULLTEXT01.pdfFilstørrelse 196 kBChecksum SHA-512
a5b64858c16fdaae5659d60483d44206010edf293cba4f2cd7beb7a5d3d1b60d22774eee49f35ea601bd3696a2d5ae240a98e75540534b33b52b6ce020d82683
Type fulltextMimetype application/pdf

Andre lenker

Forlagets fulltekst

Personposter BETA

Aronis, StavrosSagonas, Konstantinos

Søk i DiVA

Av forfatter/redaktør
Aronis, StavrosSagonas, Konstantinos
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar
Totalt: 128 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: 383 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