Validation de la compilation des boucles while DataParallel C sur des architectures à mémoire partagée

This report focuses on the compilation of the ``while'' loops in data-parallel languages for MIMD Shared Memory architectures. An efficient compilation must decrease the number of ``global synchronizations'' due to dependencies. We validate an optimization suggested by Hatcher and Quinn for the DPC language. It consists in splitting the original loop into two loops : one ``computation loop'' without any additional control dependencies, and one ``waiting loop'' to assure termination. Computation loop's body presents a minimal number of global synchronizations. We study informaly its correction proof, and give the methodology leading of its conception. The formal proof is based on the axiomatic semantics of Owiki and Gries. We give an axiomatization of the global synchronization statement, and specify which are the sufficient conditions for a non-deadlocking execution. In Hatcher and Quinn's solution, we observe that the waiting loop is independant of the computation one. The former loop absorbs residual synchronizations of any parallel program. We conclude by presenting a modular method to elaborate parallel programs.Nous etudions la compilation des boucles while des langages data-paralleles pour les architectures MIMD a memoire partagee. Une compilation efficace doit reduire le nombre de barrieres de synchronisation induites par les dependances. Nous validons une optimisation proposee par Hatcher et Quinn pour le langage DPC Elle consiste a degager une boucle de calcul sans dependances de controle supplementaires et une boucle d'attente assurant la terminaison. Le corps de la boucle de calcul contient un nombre minimal de barrieres de synchronisation. Nous etudions informellement sa correction et degageons la methode qui a permis sa conception. La preuve formelle est basee sur la semantique axiomatique dOwiki et Gries. Nous proposons une axiomatisation de la barriere de synchronisation et derivons des conditions suffisantes de non-blocage. Dans la solution de Hatcher et Quinn nous observons que la boucle d'attente est independante de la boucle de calcul et permet de resoudre un probleme plus general : l'absorption des synchronisations residuelles des programmes paralleles. Nous en deduisons une methode de conception modulaire des programmes parallele