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

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-01088655
Contributor : Sylvain Conchon <>
Submitted on : Friday, November 28, 2014 - 12:48:32 PM
Last modification on : Friday, October 4, 2019 - 1:47:31 AM
Long-term archiving on : Friday, April 14, 2017 - 10:54:31 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01088655, version 1

Collections

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. ⟨hal-01088655⟩

Share

Metrics

Record views

342

Files downloads

255