Date : 1998
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : français / French
Résumé / Abstract : 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 ramener à 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 des sections critiques, envisageant alors une version affaiblie (c'est-à-dire généralisée) de notre propriété de correction.