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

Abstract : 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.
Keywords :
Document type :
Reports
Domain :

Cited literature [18 references]

https://hal-lara.archives-ouvertes.fr/hal-02101986
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:11:24 AM
Last modification on : Wednesday, May 8, 2019 - 1:34:27 AM

### File

RR1994-13.pdf
Files produced by the author(s)

### Identifiers

• HAL Id : hal-02101986, version 1

### Citation

Gil Utard. Validation of the compilation of Data-Parallel C while'' loops for shared memory architectures. [Research Report] LIP RR-1994-13, Laboratoire de l'informatique du parallélisme. 1994, 2+21p. ⟨hal-02101986⟩

Record views