uu.seUppsala universitets publikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Verification of Software under Relaxed Memory
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för datorteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
2016 (Engelska)Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
Abstract [en]

The work covered in this thesis concerns automatic analysis of correctness of parallel programs running under relaxed memory models.

When a parallel program is compiled and executed on a modern architecture, various optimizations may cause it to behave in unexpected ways. In particular, accesses to the shared memory may appear in the execution in the opposite order to how they appear in the control flow of the original program source code. The memory model determines which memory accesses can be reordered in a program on a given system. Any memory model that allows some observable memory access reordering is called a relaxed memory model. The reorderings may cause bugs and make the production of parallel programs more difficult.

In this work, we consider three main approaches to analysis of correctness of programs running under relaxed memory models. An exact analysis for finite state programs running under the TSO memory model (Paper I). This technique is based on the well quasi ordering framework. An over-approximate analysis for integer programs running under TSO (Paper II), based on predicate abstraction combined with a buffer abstraction. Two under-approximate analysis techniques for programs running under the TSO, PSO or POWER memory models (Papers III and IV). The latter two techniques are based on stateless model checking and dynamic partial order reduction.

In addition to determining whether a program is correct under a given memory model, the problem of automatic fence synthesis is also considered. A memory fence is an instruction that can be inserted into a program in order to locally disable some memory access reorderings. The fence synthesis problem is the problem of automatically inferring a minimal set of memory fences which restores sufficient order in a given program to ensure its correctness.

Ort, förlag, år, upplaga, sidor
Uppsala: Acta Universitatis Upsaliensis, 2016. , s. 102
Serie
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1387
Nyckelord [en]
verification, relaxed memory models
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
Datavetenskap
Identifikatorer
URN: urn:nbn:se:uu:diva-297201ISBN: 978-91-554-9616-6 (tryckt)OAI: oai:DiVA.org:uu-297201DiVA, id: diva2:941290
Disputation
2016-09-07, 2446, Polacksbacken, Lägerhyddsvägen 2, Uppsala, 13:15 (Engelska)
Opponent
Handledare
Projekt
UPMARCTillgänglig från: 2016-08-17 Skapad: 2016-06-22 Senast uppdaterad: 2018-01-10
Delarbeten
1. Counter-Example Guided Fence Insertion under TSO
Öppna denna publikation i ny flik eller fönster >>Counter-Example Guided Fence Insertion under TSO
Visa övriga...
2012 (Engelska)Ingår i: Tools and Algorithms for the Construction and Analysis of Systems, Berlin: Springer-Verlag , 2012, s. 204-219Konferensbidrag, Publicerat paper (Refereegranskat)
Ort, förlag, år, upplaga, sidor
Berlin: Springer-Verlag, 2012
Serie
Lecture Notes in Computer Science ; 7214
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
urn:nbn:se:uu:diva-175078 (URN)10.1007/978-3-642-28756-5_15 (DOI)978-3-642-28755-8 (ISBN)
Konferens
TACAS 2012
Projekt
UPMARCWeak Memory Models
Tillgänglig från: 2012-03-22 Skapad: 2012-05-31 Senast uppdaterad: 2018-01-12Bibliografiskt granskad
2. Automatic fence insertion in integer programs via predicate abstraction
Öppna denna publikation i ny flik eller fönster >>Automatic fence insertion in integer programs via predicate abstraction
Visa övriga...
2012 (Engelska)Ingår i: Static Analysis, Berlin: Springer-Verlag , 2012, s. 164-180Konferensbidrag, Publicerat paper (Refereegranskat)
Ort, förlag, år, upplaga, sidor
Berlin: Springer-Verlag, 2012
Serie
Lecture Notes in Computer Science ; 7460
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
urn:nbn:se:uu:diva-175079 (URN)10.1007/978-3-642-33125-1_13 (DOI)978-3-642-33124-4 (ISBN)
Externt samarbete:
Konferens
SAS 2012
Projekt
UPMARCWeak Memory Models
Tillgänglig från: 2012-09-11 Skapad: 2012-05-31 Senast uppdaterad: 2018-01-12Bibliografiskt granskad
3. Stateless model checking for TSO and PSO
Öppna denna publikation i ny flik eller fönster >>Stateless model checking for TSO and PSO
Visa övriga...
2015 (Engelska)Ingår i: Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2015, Springer Berlin/Heidelberg, 2015, s. 353-367Konferensbidrag, Publicerat paper (Refereegranskat)
Ort, förlag, år, upplaga, sidor
Springer Berlin/Heidelberg, 2015
Serie
Lecture Notes in Computer Science ; 9035
Nationell ämneskategori
Programvaruteknik
Identifikatorer
urn:nbn:se:uu:diva-251580 (URN)10.1007/978-3-662-46681-0_28 (DOI)978-3-662-46680-3 (ISBN)
Konferens
TACAS 2015, April 11–18, London, UK
Projekt
UPMARC
Tillgänglig från: 2015-04-21 Skapad: 2015-04-21 Senast uppdaterad: 2018-01-11Bibliografiskt granskad
4. Stateless model checking for POWER
Öppna denna publikation i ny flik eller fönster >>Stateless model checking for POWER
2016 (Engelska)Ingår i: Computer Aided Verification: Part II, Springer, 2016, s. 134-156Konferensbidrag, Publicerat paper (Refereegranskat)
Abstract [en]

We present the first framework for efficient application of stateless model checking (SMC) to programs running under the relaxed memory model of POWER. The framework combines several contributions. The first contribution is that we develop a scheme for systematically deriving operational execution models from existing axiomatic ones. The scheme is such that the derived execution models are well suited for efficient SMC. We apply our scheme to the axiomatic model of POWER from [8]. Our main contribution is a technique for efficient SMC, called Relaxed Stateless Model Checking (RSMC), which systematically explores the possible inequivalent executions of a program. RSMC is suitable for execution models obtained using our scheme. We prove that RSMC is sound and optimal for the POWER memory model, in the sense that each complete program behavior is explored exactly once. We show the feasibility of our technique by providing an implementation for programs written in C/pthreads.

Ort, förlag, år, upplaga, sidor
Springer, 2016
Serie
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9780
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
urn:nbn:se:uu:diva-295424 (URN)10.1007/978-3-319-41540-6_8 (DOI)000387731400008 ()9783319415390 (ISBN)9783319415406 (ISBN)
Konferens
CAV 2016, July 17–23, Toronto, Canada
Projekt
UPMARC
Tillgänglig från: 2016-07-13 Skapad: 2016-06-07 Senast uppdaterad: 2018-01-10Bibliografiskt granskad

Open Access i DiVA

fulltext(783 kB)251 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 783 kBChecksumma SHA-512
474a84e5d49ddb6bda858df9de139bbdb1af4e0fa9cee1ab87b08f4a9fcb2ede9a932d8c8a729cd1eb421a54efa98cdef8984e8db57d626dc99839e03367fc10
Typ fulltextMimetyp application/pdf
Köp publikationen >>

Personposter BETA

Leonardsson, Carl

Sök vidare i DiVA

Av författaren/redaktören
Leonardsson, Carl
Av organisationen
Avdelningen för datorteknikDatorteknik
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 251 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

isbn
urn-nbn

Altmetricpoäng

isbn
urn-nbn
Totalt: 2736 träffar
RefereraExporteraLänk till posten
Permanent länk

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