Abstract FR:

Cette these est composee de trois parties. 1) la validation des applications data-paralleles. 2) l'etude et la validation d'un schema de compilation. 3) l'etude de la faisabilite de l'integration de mecanismes d'equilibrage de charge au niveau du schema d'execution. Dans la premiere partie, nous avons developpe une semantique axiomatique pour un langage data-parallele minimal, appele l. Cette semantique permet de definir un systeme de preuve. Un resultat fondamental et non trivial sur sa completude est donne. Cette semantique est ensuite etendue aux structures de controle complexes que l'on peut trouver dans les langages reels. Dans la deuxieme partie, nous donnons la preuve formelle d'une optimisation de compilation des boucles data-paralleles du langage dpc. La preuve est obtenue par une extension de la semantique axiomatique des langages paralleles. Il en resulte une methode de conception modulaire de programmes paralleles. Dans la troisieme partie, nous presentons une implementation de mecanismes de reequilibrages de charge dans les programmes data-paralleles compiles par la methode de virtualisation. Le principe est la migration des processeurs virtuels. Nous presentons ainsi un prototype de compilateur c* pour reseau de stations sous pvm