Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Thèses et habilitations
Production scientifique
Doctorat de

Doctorat
Equipe : Vérification d'Algorithmes, Langages et Systèmes

Vérification par Model Checking de Programmes Concurrents Paramétrés sur des Modèles de Mémoire Faibles

Début le 01/10/2014
Direction : ZAIDI, Fatiha

Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Sud

Lieu de déroulement : LRI - VALS

Soutenue le 24/09/2018 devant le jury composé de :
Directrice de thèse :
- Mme. Fatiha Zaïdi (Université Paris-Sud)

Co-encadrant :
- M. Sylvain Conchon (Université Paris-Sud)

Rapporteurs :
- M. Ahmed Bouajjani (Université Paris Diderot)
- M. Dominique Méry (Université de Lorraine)

Examinateurs :
- M. Luc Maranget (INRIA Paris)
- M. Philippe Quéinnec (Toulouse INP - ENSEEIHT)

Activités de recherche :

Résumé :
Les multiprocesseurs et microprocesseurs multicœurs modernes mettent en oeuvre des modèles mémoires dits faibles ou relâchés, dans lesquels l'ordre apparent des opérations mémoires ne suit pas la cohérence séquentielle (SC) proposée par Leslie Lamport. Tout programme concurrent s'exécutant sur une telle architecture et conçu avec un modèle SC en tête risque de montrer à l'exécution de nouveaux comportements, dont certains sont potentiellement des comportements incorrects. Par exemple, un algorithme d'exclusion mutuelle correct avec une sémantique par entrelacement pourrait ne plus garantir l'exclusion mutuelle lorsqu'il est mis en oeuvre sur une architecture plus relâchée.

Raisonner sur la sémantique de tels programmes s'avère très difficile. Par ailleurs, bon nombre d'algorithmes concurrents sont conçus pour fonctionner indépendamment du nombre de processus mis en oeuvre. On voudrait donc pouvoir s'assurer de la correction d'algorithmes concurrents, quel que soit le nombre de processus impliqués. Pour ce faire, on s'appuie sur le cadre du Model Checking Modulo Theories (MCMT), développé par Ghilardi et Ranise, qui permet la vérification de propriétés de sûreté de programmes concurrents paramétrés, c'est-à-dire mettant en oeuvre un nombre arbitraire de processus. On étend cette technologie avec une théorie permettant de raisonner sur des modèles mémoires faibles. Le résultat ce ces travaux est une extension du model checker Cubicle, appelée Cubicle-W, permettant de vérifier des propriétés de systèmes de transitions paramétrés s'exécutant sur un modèle mémoire faible similaire à TSO.