Verification by Abstract Interpretation Under Weakly Consistent Memory
Static analysis aims to certify critical software by establishing the absence of errors amongst every possible execution of a given program. Abstract interpretation provides a general theoretical framework to build such analysis that are sound-by-design: they take every possible behaviour of the target into account. In this thesis, we address the verification of concurrent programs that run in weakly consistent memory models. In addition to sequentially consistent executions that match the interleavings of the threads, these models allow counter-intuitive behaviours that further complicate human reasoning. We propose dedicated abstract domains to analyse the programs that run under such models. Supported by experimental results, we show how these domains, by means of adapted iteration methods, allow precisely verifying the correction of typical concurrent programming algorithms. To improve the scaling, we extend this work to the design of a thread-modular analysis. We show by experimentations how, by leveraging specific abstractions and an optimised iteration strategy, this method allows efficiently analysing programs that involve a greater number of threads. We eventually define abstract domains allowing to precisely infer relations that are specific to the memory model, in order to certify programs entailing complex invariants.
答辩 : 2019-2-26 - 14h - Salle W, École Normale Supérieure : 45 rue d'Ulm, 75005 Paris 评委会 : M. David Pichardie (ENS Rennes, Irisa), [Rapporteur]
M. David Monniaux (Verimag, CNRS), [Rapporteur]
M. Antoine Miné (LIP6, Sorbonne Université)
M. Emmanuel Chailloux (LIP6, Sorbonne Université)
M. Luc Maranget (Inria Paris)
M. Xavier Rival (École normale supérieure, Inria)