, De m^ eme, on observait que ce sch ema d'absorption des synchronisations pouvait ^ etre employ e pour tout programme parall ele ayant subi une transformation simple, D'autre part, nous avons observ e que cet absorbeur pouvait ^ etre employ e pour toutes les boucles DPC ayant u n n o m bre de d ependances quelconque

. Ennn, un programme parall ele quelconque pouvaient ^ etre compos es s equentiellement par l'interm ediaire d'une barri ere de synchronisation, nous avons donc d egag e une m ethode de conception modulaire des programmes parall eles

, qui est equivalente a l'absence de blocage, permet de d evelopper des modules ind ependants de programmes distribu es. Mais, en l'absence de canal de communication particulier, la preuve d e (( fermeture )) doit ^ etre faite pour chaque module. Ici, gr^ ace a l'existence d'absorbeurs simples, il est possible de d evelopper chaque module sans s

, Comme le principal sujet d' etude est la trace des synchronisations, on peut envisager une approche par une s emantique observationnelle de type CCS. La synchronisation serait une action particuli ere dont l e m ecanisme r esiderait dans le masquage. Un absorbeur de synchonisations serait un op erateur particulier sur l'alg ebre des processus, mod elisant une barri ere de synchronisation, Dans cette etude nous avons employ e une m ethode de preuve axiomatique

, L'analyse des propri et es alg ebriques permettrait peut-^ etre de formaliser de mani ere plus ais ee le processus de transformation des structures de contr^ ole de la compilation d'un programme dataparall ele

. Remerciements, Je remercie Luc Boug e e t J o a c him Gabarrr o pour leurs commentaires sur ce travail

K. R. Apt and E. R. Olderog, Veriication of Sequential and Concurrent Programs. T ext and Monographs in Computer Science, 1990.

L. Boug, Modularit e e t S y m etrie pour les Syst emes R epartis : Application au Langage CSP. Laboratoire d'Informatique de L'Ecole Normale Sup erieure, 1987.

L. Boug, Mod ele de programmation a parall elisme de donn ees : une perspective s emantique. Technique et science informatiques, vol.12, pp.541-562, 1993.

T. Elrad and N. Francez, Decomposition of distributed programs into communication-closed layers, Science of Computer Programming, vol.2, pp.155-173, 1982.

, High Performance F ortran language speciication (draft version), 1993.

R. Gerth and L. Shrira, On proving communication closedness of distributed layers, Sixth conf. of FST/TCS, n umber 241 in LNCS, pp.330-343, 1986.

P. J. Hatcher and M. J. Quinn, Data-Parallel Programming on MIMD Computers. Scientiic and Engineering Computation, 1991.

E. A. Heinz and M. Philippsen, Synchronization Barrier Elimination in Synchronous FORALLs, 1993.

, Ecole Polytechnique Projet X-P^ ole 91128 Palaiseau Cedex France. Hyper C Documentation, 1993.

, Maspar Parallel Application Language Reference Manual, 1990.

S. Owiki and D. Gries, Verifying Properties of Parallel Programs: An Axiomatic Approach, Communications of the ACM, vol.19, issue.5, pp.279-285, 1976.

, Thinking Machine Corporation, Cambridge MA. C programming guide, pp.1-9