Validation of the compilation of Data-Parallel C ``while'' loops for shared memory architectures

(eng) 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