Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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
Counter-Example Guided Fence Insertion under TSO
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, Datorteknik.
Visa övriga samt affilieringar
2012 (Engelska)Ingår i: Tools and Algorithms for the Construction and Analysis of Systems, Berlin: Springer-Verlag , 2012, 204-219 s.Konferensbidrag, Publicerat paper (Refereegranskat)
Ort, förlag, år, upplaga, sidor
Berlin: Springer-Verlag , 2012. 204-219 s.
Serie
Lecture Notes in Computer Science, 7214
Nationell ämneskategori
Datavetenskap (datalogi)
Identifikatorer
URN: urn:nbn:se:uu:diva-175078DOI: 10.1007/978-3-642-28756-5_15ISBN: 978-3-642-28755-8 (tryckt)OAI: oai:DiVA.org:uu-175078DiVA: diva2:530090
Konferens
TACAS 2012
Projekt
UPMARCWeak Memory Models
Tillgänglig från: 2012-03-22 Skapad: 2012-05-31 Senast uppdaterad: 2016-08-22Bibliografiskt granskad
Ingår i avhandling
1. Verification of Software under Relaxed Memory
Öppna denna publikation i ny flik eller fönster >>Verification of Software under Relaxed Memory
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. 102 s.
Serie
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1387
Nyckelord
verification, relaxed memory models
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
Datavetenskap
Identifikatorer
urn:nbn:se:uu:diva-297201 (URN)978-91-554-9616-6 (ISBN)
Externt samarbete:
Disputation
2016-09-07, 2446, Polacksbacken, Lägerhyddsvägen 2, Uppsala, 13:15 (Engelska)
Opponent
Handledare
Projekt
UPMARC
Tillgänglig från: 2016-08-17 Skapad: 2016-06-22 Senast uppdaterad: 2016-08-25

Open Access i DiVA

fulltext(518 kB)109 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 518 kBChecksumma SHA-512
05477bd437c6bd5cca6f57197e48846faf790903ada2fc3b1e527b4c5bc235169a6ba257bfc839321099299208724f225c81bc36247e73f9b999cc5c58a90a0f
Typ fulltextMimetyp application/pdf

Övriga länkar

Förlagets fulltext

Personposter BETA

Abdulla, Parosh AzizAtig, Mohamed FaouziLeonardsson, Carl

Sök vidare i DiVA

Av författaren/redaktören
Abdulla, Parosh AzizAtig, Mohamed FaouziLeonardsson, Carl
Av organisationen
Datorteknik
Datavetenskap (datalogi)

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 109 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.

doi
isbn
urn-nbn

Altmetricpoäng

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

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • 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