Dossier de Mohamed Faouzi Atig

Informations sur la thèse

Vérification de Programmes Concurrents: Décidabilité et Complexité

Thèse de doctorat commencée le 01/10/2006 et soutenue à Paris, le 07/06/2010.

Diplôme délivré par Université Paris Diderot- Paris 7. Préparé dans le(s) laboratoire(s) suivant(s) :

Laboratoire d'Informatique Algorithmique: Fondements et Applications (CNRS UMR 7089, Université Paris Diderot – Paris 7)

Sous la direction de :

Thèse soutenue devant un jury composé de :

président : Wieslaw Zielonka, Université Paris Diderot- Paris 7
rapporteur : Javier Esparza, Université de Munich
rapporteur : Jean-François Raskin, Université Libre de Bruxelles
membre : Joêl Ouknine, Université d'Oxford
membre : Philippe Schnoebelen, Directeur de recherche CNRS
Co-Directrice: Tayssir Touili, Chargée de recherche CNRS
Directeur: Ahmed Bouajjani, Université Paris Diderot – Paris 7

Documents associés

Résumé de la thèse

Cette thèse traite du problème de la vérification de programmes concurrents, et en particulier des questions de la décidabilité et de la complexité de ce problème. Les programmes concurrents sont en effet de plus en plus utilisés à différents niveaux dans les systèmes informatiques, allant des applications distribuées sur les réseaux de grande taille aux logiciels de base pour les architectures matérielles multi-coeurs, en passant par les systèmes d'exploitation multi-tâches et la programmation multi-thread. La conception de ces programmes posent de nombreux problèmes dus à l'énorme complexité de leurs comportements.

Dans une première partie de la thèse, nous considérons le cas de programmes concurrents avec appels de procédures (potentiellement récursives et/ou création dynamique de processus). Le problème de la vérification (accessibilité par exemple) est indécidable en général pour de tels programmes. Nous étudions alors des algorithmes d'analyse sous-approchée, basées sur une notion pertinente pour le choix des comportements à analyser et offrant une couverture aussi large que possible des comportements, permettant ainsi de détecter de manière efficace les erreurs (bugs) dans ces programmes. Nous proposons pour cela des modèles formels basés sur des réseaux d'automates à pile communicants, et nous étudions la décidabilité et la complexité du problème de l'accessibilité sous certaines restrictions sur les comportements de ces modèles. Nos résultats généralisent plusieurs travaux menés aussi bien dans la communauté de la vérification ([Qadeer et Rehof, TACAS'05], [La Torre et al., LICS'07] sur le `context/phase-bounded analysis'') que dans la communauté de la théorie des automates ([Breveglieri et al., IJFCS'96] sur les automates à multi-piles ordonnés).

Nous étudions dans une seconde partie de la thèse le problème de la vérification de programmes s'exécutant selon des modèles faibles de la mémoire partagée, dans lesquels certaines actions (de lecture et d'écriture) peuvent être réordonnées (par le matériel ou par le compilateur) pour des raisons de performance. La décidabilité de ce problème n'est pas triviale car le réordonnancement d'actions définit en général des ensembles non-réguliers de comportements. Nous proposons des modèles formels basés sur les automates à canaux FIFO pour certains de ces modèles de mémoire, et nous étudions pour la première fois les limites de la décidabilité et la complexité des problèmes de vérification (accessibilité, accessibilité répétée) pour ces modèles. Nous prouvons notamment que le problème de l'accessibilité pour les modèles de mémoire TSO/PSO est décidable mais de complexité non récursive primitive, alors que pour certains modèles plus faibles (avec spéculations sur les lectures), ce problème devient indécidable.

Les résultats de décidabilité et de complexité que nous avons obtenus, aussi bien dans la première que dans la seconde partie de la thèse, sont de manière générale établis grâce à un raisonnement compositionnel, permettant de réduire ces problèmes d'accessibilité considérés à des problèmes analogues sur des modèles tels que les réseaux de Petri, ou les systèmes communicants à travers des canaux non fiables (avec pertes).

En cas de problème avec ce dossier, contactez le secrétaire du prix Mathieu Giraud