Change search
ReferencesLink to record
Permanent link

Direct link
Verification of Software under Relaxed Memory
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2016 (English)Doctoral thesis, comprehensive summary (Other academic)
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.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2016. , 102 p.
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1387
Keyword [en]
verification, relaxed memory models
National Category
Computer Science
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:uu:diva-297201ISBN: 978-91-554-9616-6OAI: oai:DiVA.org:uu-297201DiVA: diva2:941290
Public defence
2016-09-07, 2446, Polacksbacken, Lägerhyddsvägen 2, Uppsala, 13:15 (English)
Opponent
Supervisors
Projects
UPMARC
Available from: 2016-08-17 Created: 2016-06-22 Last updated: 2016-08-25
List of papers
1. Counter-Example Guided Fence Insertion under TSO
Open this publication in new window or tab >>Counter-Example Guided Fence Insertion under TSO
Show others...
2012 (English)In: Tools and Algorithms for the Construction and Analysis of Systems, Berlin: Springer-Verlag , 2012, 204-219 p.Conference paper (Refereed)
Place, publisher, year, edition, pages
Berlin: Springer-Verlag, 2012
Series
, Lecture Notes in Computer Science, 7214
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-175078 (URN)10.1007/978-3-642-28756-5_15 (DOI)978-3-642-28755-8 (ISBN)
Conference
TACAS 2012
Projects
UPMARCWeak Memory Models
Available from: 2012-03-22 Created: 2012-05-31 Last updated: 2016-08-22Bibliographically approved
2. Automatic fence insertion in integer programs via predicate abstraction
Open this publication in new window or tab >>Automatic fence insertion in integer programs via predicate abstraction
Show others...
2012 (English)In: Static Analysis, Berlin: Springer-Verlag , 2012, 164-180 p.Conference paper (Refereed)
Place, publisher, year, edition, pages
Berlin: Springer-Verlag, 2012
Series
, Lecture Notes in Computer Science, 7460
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-175079 (URN)10.1007/978-3-642-33125-1_13 (DOI)978-3-642-33124-4 (ISBN)
External cooperation:
Conference
SAS 2012
Projects
UPMARCWeak Memory Models
Available from: 2012-09-11 Created: 2012-05-31 Last updated: 2016-08-26Bibliographically approved
3. Stateless model checking for TSO and PSO
Open this publication in new window or tab >>Stateless model checking for TSO and PSO
Show others...
2015 (English)In: Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2015, Springer Berlin/Heidelberg, 2015, 353-367 p.Conference paper (Refereed)
Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2015
Series
, Lecture Notes in Computer Science, 9035
National Category
Software Engineering
Identifiers
urn:nbn:se:uu:diva-251580 (URN)10.1007/978-3-662-46681-0_28 (DOI)978-3-662-46680-3 (ISBN)
Conference
TACAS 2015, April 11–18, London, UK
Projects
UPMARC
Available from: 2015-04-21 Created: 2015-04-21 Last updated: 2016-08-22Bibliographically approved
4. Stateless model checking for POWER
Open this publication in new window or tab >>Stateless model checking for POWER
2016 (English)In: Computer Aided Verification: Part II, Springer, 2016, 134-156 p.Conference paper (Refereed)
Place, publisher, year, edition, pages
Springer, 2016
Series
, Lecture Notes in Computer Science, 9780
National Category
Computer Science
Identifiers
urn:nbn:se:uu:diva-295424 (URN)10.1007/978-3-319-41540-6_8 (DOI)978-3-319-41539-0 (ISBN)
Conference
CAV 2016, July 17–23, Toronto, Canada
Projects
UPMARC
Available from: 2016-07-13 Created: 2016-06-07 Last updated: 2016-08-22Bibliographically approved

Open Access in DiVA

fulltext(783 kB)66 downloads
File information
File name FULLTEXT01.pdfFile size 783 kBChecksum SHA-512
474a84e5d49ddb6bda858df9de139bbdb1af4e0fa9cee1ab87b08f4a9fcb2ede9a932d8c8a729cd1eb421a54efa98cdef8984e8db57d626dc99839e03367fc10
Type fulltextMimetype application/pdf
Buy this publication >>

Search in DiVA

By author/editor
Leonardsson, Carl
By organisation
Division of Computer SystemsComputer Systems
Computer Science

Search outside of DiVA

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

Total: 1670 hits
ReferencesLink to record
Permanent link

Direct link