Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs

Antoine Miné 1, 2
2 ABSTRACTION - Abstract Interpretation and Static Analysis
CNRS - Centre National de la Recherche Scientifique : UMR 8548, Inria Paris-Rocquencourt, DI-ENS - Département d'informatique de l'École normale supérieure
Abstract : We present a static analysis by Abstract Interpretation to check for run-time errors in parallel C programs. Following our work on Astrée, we focus on embedded critical programs without recursion nor dynamic memory allocation, but extend the analysis to a static set of threads. Our method iterates a slightly modified non-parallel analysis over each thread in turn, until thread interferences stabilize. We prove the soundness of the method with respect to a sequential consistent semantics and a reasonable weakly consistent memory semantics. We then show how to take into account mutual exclusion and thread priorities through partitioning over the scheduler state. We present preliminary experimental results analyzing a real program with our prototype, Thésée, and demonstrate the scalability of our approach.
Type de document :
Communication dans un congrès
Gilles Barthe. ESOP'11 - 20th European Symposium on Programming, Mar 2011, Saarbrücken, Germany. Springer, 6602, pp.398-418, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-19718-5_21〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00648038
Contributeur : Antoine Miné <>
Soumis le : dimanche 4 décembre 2011 - 23:18:13
Dernière modification le : mardi 24 avril 2018 - 17:20:13
Document(s) archivé(s) le : vendredi 16 novembre 2012 - 14:21:24

Fichier

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

Identifiants

Collections

Citation

Antoine Miné. Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs. Gilles Barthe. ESOP'11 - 20th European Symposium on Programming, Mar 2011, Saarbrücken, Germany. Springer, 6602, pp.398-418, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-19718-5_21〉. 〈hal-00648038〉

Partager

Métriques

Consultations de la notice

361

Téléchargements de fichiers

129