Relational interprocedural analysis of concurrent programs

Abstract : We extend the relational approach to interprocedural analysis of sequential programs to concurrent programs composed of a fixed number of threads. In the relational approach, a sequential program is analyzed by computing summaries of procedures, and by propagating reachability information using these summaries. We generalize this approach to concurrent programs by computing for each thread procedure summaries that takes into account the parallel execution of the other threads. Technically, we define our analysis method by instrumenting the operational semantics of programs, then by abstracting the call-stacks of the concurrent threads, and last by abstracting the program environments in order to lead to an effective analysis that always terminates. This method allows to extend to concurrent programs existing relational interprocedural analysis (e.g., numerical variables analysis, shape analysis). We implemented it for programs with scalar variables, and we experiment several classical synchronisation protocols in order to illustrate the precision of our technique, but also to analyze the approximations it performs.
Type de document :
Rapport
[Research Report] RR-6671, INRIA. 2008, pp.36
Liste complète des métadonnées

https://hal.inria.fr/inria-00328045
Contributeur : Bertrand Jeannet <>
Soumis le : jeudi 9 octobre 2008 - 16:09:56
Dernière modification le : jeudi 11 octobre 2018 - 08:48:01
Document(s) archivé(s) le : lundi 7 juin 2010 - 17:53:40

Fichier

RR-6671.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00328045, version 1

Collections

Citation

Bertrand Jeannet. Relational interprocedural analysis of concurrent programs. [Research Report] RR-6671, INRIA. 2008, pp.36. 〈inria-00328045〉

Partager

Métriques

Consultations de la notice

271

Téléchargements de fichiers

148