Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions

Raphaël Monat 1, 2 Antoine Miné 3
2 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt
3 APR - Algorithmes, Programmes et Résolution
LIP6 - Laboratoire d'Informatique de Paris 6
Abstract : We present a static analysis by abstract interpretation of numeric properties in multi-threaded programs. The analysis is sound (assuming a sequentially consistent memory), parameterized by a choice of abstract domains and, in order to scale up, it is modular, in that it iterates over each thread individually (possibly several times) instead of iterating over their product. We build on previous work that formalized rely-guarantee verification methods as a concrete, fixpoint-based semantics, and then apply classic numeric abstractions to abstract independently thread states and thread interference. This results in a flexible algorithm allowing a wide range of precision versus cost trade-offs, and able to infer even flow-sensitive and relational thread interference. We implemented our method in an analyzer prototype for a simple language and experimented it on several classic mutual exclusion algorithms for two or more threads. Our prototype is instantiated with the polyhedra domain and employs simple control partitioning to distinguish critical sections from surrounding code. It relates the variables of all threads using polyhedra, which limits its scalability in the number of variables. Nevertheless, preliminary experiments and comparison with ConcurInterproc show that modularity enables scaling to a large number of thread instances, provided that the total number of variables stays small.
Type de document :
Communication dans un congrès
Ahmed Bouajjani; David Monniaux. Verification, Model Checking, and Abstract Interpretation (VMCAI) 2017, Jan 2017, Paris, France. Springer, Verification, Model Checking, and Abstract Interpretation, 10145, pp.386-404, 2017, Lecture Notes in Computer Science. 〈http://conf.researchr.org/track/VMCAI-2017/〉. 〈10.1007/978-3-319-52234-0_21〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01490178
Contributeur : Raphaël Monat <>
Soumis le : mardi 14 mars 2017 - 23:36:03
Dernière modification le : vendredi 25 mai 2018 - 12:02:07
Document(s) archivé(s) le : jeudi 15 juin 2017 - 15:15:58

Fichier

vmcai17.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Raphaël Monat, Antoine Miné. Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions. Ahmed Bouajjani; David Monniaux. Verification, Model Checking, and Abstract Interpretation (VMCAI) 2017, Jan 2017, Paris, France. Springer, Verification, Model Checking, and Abstract Interpretation, 10145, pp.386-404, 2017, Lecture Notes in Computer Science. 〈http://conf.researchr.org/track/VMCAI-2017/〉. 〈10.1007/978-3-319-52234-0_21〉. 〈hal-01490178〉

Partager

Métriques

Consultations de la notice

311

Téléchargements de fichiers

83