UNIVERSITÄTSBIBLIOTHEK

Verification with Memory Models as Input

  • To improve efficiency of memory accesses, modern multiprocessor architectures implement a whole range of different weak memory models. The behavior of performance-critical code depends on the underlying hardware. There is a rising demand for verification tools that take the underlying memory model into account. This work examines a variety of prevalent problems in the field of program verification of increasing complexities: testing, reachability, portability and memory model synthesis. We give efficient tools to solve these problems. What sets the presented methods apart is that they are not limited to some few given architectures. They are universal: The memory model is given as part of the input. We make use of the CAT language to succinctly describe axiomatic memory models. CAT has been used to define the semantics of assembly for x86/TSO, ARMv7, ARMv8, and POWER but also the semantics of programming languages such as C/C++, including the Linux kernel concurrency primitives. This work shows that even the simple testing problem is NP-hard for most memory models. It does so using a general reduction technique that applies to a range of models. It examines the more difficult program verification under a memory model and introduces Dartagnan, a bounded model checker (BMC) that encodes the problem as an SMT-query and makes use of advanced encoding techniques. The program portability problem is shown to be even harder. Despite this, it is solved efficiently by the tool Porthos which uses a guided search to produce fast results for most practical instances. A memory model is synthesized by Aramis for a given set of reachability results. Concurrent program verification is generally undecidable even for sequential consistency. As an alternative to BMC, we propose a new CEGAR method for Petri net invariant synthesis. We again use SMT-queries as a back-end.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Florian Furbach
URN (permanent link):urn:nbn:de:hbz:386-kluedo-63678
DOI:https://doi.org/10.26204/KLUEDO/6367
Advisor:Roland Meyer
Document Type:Doctoral Thesis
Language of publication:English
Publication Date:2021/05/19
Year of Publication:2021
Publishing Institute:Technische Universität Kaiserslautern
Granting Institute:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2020/11/10
Date of the Publication (Server):2021/05/19
Number of page:IX, 195
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Creative Commons 4.0 - Namensnennung, nicht kommerziell, keine Bearbeitung (CC BY-NC-ND 4.0)