THÈSE D'UNIVERSITÉ : Contribution à la modélisation du SPMD : distribution asynchrone d'automates

Fichier PostScript (309K)

Benoît Caillaud

juin 1994

Cette thèse porte sur la caractérisation des comportements des programmes répartis SPMD, produits par distribution automatique de programmes séquentiels. Il s'agit d'un travail de modélisation s'appuyant sur deux outils théoriques : la théorie des ensembles ordonnés et les semi-commutations. L'ensemble des comportements d'un programme SPMD est représenté par une structure adéquate, un automate d'ordres.

Les résultats obtenus s'appliquent aussi bien aux programmes séquentiels impératifs qu'aux programmes réactifs synchrones. Un cadre formel pour la preuve de correction de schémas de répartitions est proposé et appliqué sur un exemple complet : la preuve de correction d'un schéma de répartition de programmes séquentiels impératifs.

La dernière partie porte sur la caractérisation de l'asynchronisme et du comportement des canaux de communications d'une classe particulière de programmes SPMD. Les résultats établis permettent de décider de la bornitude de l'asynchronisme et des canaux de communication.

PhD THESIS:
Modelization of SPMD Programs: Distributing Automata for Asynchronous Networks of Processors

PostScript file (309K)

Benoît Caillaud

June 1994

The aim of this thesis is the behavioural study of SPMD distributed programs, which are produced by automatic distribution of sequential programs. The results detailed in this thesis can be applied to both sequential imperative and synchronous reactive programs. A formal framework for correctness proofs of distribution schemes is detailed and applied on the correctness proof of a real distribution scheme of sequential imperative programs.

Two theoretical tools are used: partially ordered set theory and semi-commutations. The set of all possible behaviors of SPMD programs is coded by structures called order automata.

Then asynchronism and communication channel behavior of a subclass of SPMD programs are characterized. Asynchronism boundness and communication channel boundness are decidable in this class of SPMD programs. Two decision criteria are given.