Validation of the compilation of Data-Parallel C ``while'' loops for shared memory architectures - LARA - Libre accès aux rapports scientifiques et techniques Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1994

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

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

Gil Utard

Résumé

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 paralleles
Fichier principal
Vignette du fichier
RR1994-13.pdf (272.76 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02101986 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02101986 , version 1

Citer

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⟩
19 Consultations
23 Téléchargements

Partager

Gmail Mastodon Facebook X LinkedIn More