Propriétés de correction séquentielle dans un langage parallèle à mémoire partagée - Archive ouverte HAL Access content directly
Theses Year : 1998

Propriétés de correction séquentielle dans un langage parallèle à mémoire partagée

(1)
1

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 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).
Fichier principal
Vignette du fichier
tel-00005591.pdf (712.24 Ko) Télécharger le fichier

Dates and versions

tel-00005591 , version 1 (05-04-2004)

Identifiers

  • HAL Id : tel-00005591 , version 1

Cite

Gilbert Caplain. Propriétés de correction séquentielle dans un langage parallèle à mémoire partagée. Réseaux et télécommunications [cs.NI]. Ecole des Ponts ParisTech, 1998. Français. ⟨NNT : ⟩. ⟨tel-00005591⟩
183 View
305 Download

Share

Gmail Facebook Twitter LinkedIn More