La norme C11 du langage C prend en charge la programmation avec threads sur architectures multi-coeurs. En particulier, elle introduit une notion de variables atomiques, ainsi qu'un système primitif de barrières de synchronisation (Acquire/Release fendes).
Dans cette thèse, on s'intéressera à la vérification par des techniques de test et model checking de programmes C11 avec threads pour des architectures à mémoire faible diverses. Pour cela, on utilisera le model checker Cubicle développé dans l'équipe Vals. Cubicle est basé sur une nouvelle technique de model checking qui repose sur la démonstration automatique SMT (Satisfiability Modulo Theories).
Context
La mise au point des programmes C concurrents est très difficile. Outre le non-déterminisme inhérent à ce style de programmation, le langage ne fournit pas assez d'information sur l'atomicité des opérations ou la gestion de la mémoire pour garantir la bonne exécution d'un programme contenant des threads. Ceci est d'autant plus aggravé par les modèles à mémoire faible des architectures modernes.
La dernière norme C11 du langage C tente de remédier à cette situation en prenant en charge le multi-threading. En particulier, elle introduit une notion de variables atomiques, ainsi qu'un système primitif de barrières de synchronisation (Acquire/Release fences) pour écrire des programmes concurrents sur architectures multi-coeurs.
Objectives
L'objectif de cette thèse est la vérification formelle de propriétés de sûreté de programmes C11 par model checking. Cette technique de vérification tente de vérifier la sûreté d'un programme concurrent en explorant (statiquement) tous ses comportements possibles à l'exécution.
En particulier, on s'intéressera à garantir la non-atteignabilité d'états indésirables pour des programmes faisant intervenir un nombre quelconque de threads et/ou basés sur des architectures à mémoire faible diverses.
Pour cela, on utilisera le model checker Cubicle développé dans l'équipe Vals. Cubicle est basé sur une nouvelle technique de model checking qui repose sur la démonstration automatique SMT (Satisfiability Modulo Theories).
Cubicle sera également utilisé par des techniques de génération de contre-exemple pour la génération de tests.
Work program
Extra information
Prerequisite
Connaissances en test, model checking, démonstration automatique, compilation
Détails
Expected funding
Institutional funding
Status of funding
Expected
Candidates
David Declerck
Utilisateur
sylvain.conchon
Créé
Lundi 19 mai 2014 22:57:18 CEST
dernière modif.
Vendredi 06 juin 2014 17:53:14 CEST
Fichiers joints
filename
créé
hits
filesize
Aucun fichier joint à cette fiche
Connexion
Ecole Doctorale Informatique Paris-Sud
Directrice
Nicole Bidoit Assistante
Stéphanie Druetta Conseiller aux thèses
Dominique Gouyou-Beauchamps
ED 427 - Université Paris-Sud
UFR Sciences Orsay
Bat 650 - aile nord - 417
Tel : 01 69 15 63 19
Fax : 01 69 15 63 87
courriel: ed-info à lri.fr