Skip to Main content Skip to Navigation
Theses

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).
Complete list of metadatas

https://pastel.archives-ouvertes.fr/tel-00005591
Contributor : Admin Pastel <>
Submitted on : Monday, April 5, 2004 - 5:31:24 PM
Last modification on : Tuesday, April 24, 2018 - 1:30:27 PM
Long-term archiving on: : Friday, April 2, 2010 - 9:02:30 PM

Identifiers

  • HAL Id : tel-00005591, version 1

Collections

Citation

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. ⟨tel-00005591⟩

Share

Metrics

Record views

444

Files downloads

260