Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières

Sylvain Conchon 1, 2 Luc Maranget 3 Alain Mebsout 1 David Declerck 1
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Résumé : Toutes les bibliothèques de threads au standard POSIX se doivent d'\implementer une barrière de synchronisation. Une telle structure de contrôle permet à des threads de s'attendre en un point donné d'un programme. Il existe de nombreuses implémentations pour ces barrières, plus ou moins sophistiquées. Citons par exemple, les sense barriers, les static tree barriers, les tournament barriers, etc.Nous présentons dans cet article un outil pour vérifier automatiquement la sûreté de barrières de synchronisation écrites en langage C. Pour être sûre, une barrière doit garantir qu'aucun thread ne peut la franchir tant que les autres ne l'ont pas atteinte, et ceci quelque soit le nombre de threads impliqués.Notre approche consiste à compiler des programmes C avec threads vers des systèmes de transition paramétrés, puis à vérifier leur sûreté à l'aide d'un model checker. Plus concrètement, notre compilateur traduit un sous-ensemble du C vers le langage d'entrée de Cubicle.On montre le bien fondé de notre technique par la preuve de sûreté de la barrière sense reversing pour un nombre quelconque de threads. À notre connaissance, c'est la première preuve automatique d'une telle implémentation.
Type de document :
Communication dans un congrès
JFLA, Jan 2014, Fréjus, France. 2014
Liste complète des métadonnées


https://hal.inria.fr/hal-01088655
Contributeur : Sylvain Conchon <>
Soumis le : vendredi 28 novembre 2014 - 12:48:32
Dernière modification le : jeudi 9 février 2017 - 15:53:02
Document(s) archivé(s) le : vendredi 14 avril 2017 - 22:54:31

Fichier

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

Identifiants

  • HAL Id : hal-01088655, version 1

Citation

Sylvain Conchon, Luc Maranget, Alain Mebsout, David Declerck. Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières. JFLA, Jan 2014, Fréjus, France. 2014. <hal-01088655>

Partager

Métriques

Consultations de
la notice

210

Téléchargements du document

109