Skip to Main content Skip to Navigation
Reports

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

Résumé : 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
Document type :
Reports
Complete list of metadatas

Cited literature [18 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101986
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:11:24 AM
Last modification on : Thursday, November 21, 2019 - 2:38:40 AM

File

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

Identifiers

  • HAL Id : hal-02101986, version 1

Collections

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⟩

Share

Metrics

Record views

14

Files downloads

16