Propriétés de correction séquentielle dans un langage parallèle à mémoire partagée
Résumé
Nous étudions une propriété de correction de programmes écrits dans un langage parallèle. Cette propriété est une équivalence sémantique entre le programme parallèle et sa version séquentielle, que nous définissons. Le langage que nous considérons, outre des structures séquentielles usuelles (boucles, branchements conditionnels), comporte des boucles parallèles et des synchronisations par événements. L'objet principal de cette thèse est de démontrer un théorème qui assure cette propriété de correction, sous un certain nombre d'hypothèses, principalement une condition de préservation des dépendances de données. Ces hypothèses portent seulement sur la sémantique de la version séquentielle : autrement dit, en vertu de notre résultat, vérifier la correction d'un certain programme parallèle se ramène à vérifier un certain nombre de propriétés de sa seule version séquentielle. Par ailleurs, nous esquissons une extension de ce résultat, par l'introduction de sections critiques, envisageant alors une version affaiblie (c'est-à-dire généralisée) de notre propriété de correction. (Résumé de l'auteur).