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

National audienceToutes 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