Verification of Software under Relaxed Memory

• Main Author: Leonardsson, Carl
• Format: Doctoral Thesis
• Language: English
• Published: Uppsala universitet, Avdelningen för datorteknik 2016
• Subjects: verification; relaxed memory models
• Online Access: http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-297201; http://nbn-resolving.de/urn:isbn:978-91-554-9616-6

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. === UPMARC