Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières - Archive ouverte HAL Access content directly
Conference Papers Year : 2014

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

(1, 2) , (3) , (1) , (1)
1
2
3

Abstract

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.
Fichier principal
Vignette du fichier
main.pdf (397.18 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01088655 , version 1 (28-11-2014)

Identifiers

  • HAL Id : hal-01088655 , version 1

Cite

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. ⟨hal-01088655⟩
181 View
114 Download

Share

Gmail Facebook Twitter LinkedIn More