Escape constructs in data-parallel languages: semantics and proof system - Archive ouverte HAL Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1994

Escape constructs in data-parallel languages: semantics and proof system

Luc Bougé
Gil Utard

Résumé

We describe a simple data-parallel kernel language which encapsulates the main data-parallel control structures found in high-level languages such as MasPar's MPL or the recent HyperC. In particular, it includes the concept of data-parallel escape, which extends the break and continue constructs of the scalar C language. We give this language a natural semantics, we define a notion of assertion and describe an assertional proof system. We demonstrate its use by proving a small data-parallel Mandelbrot-like program.
Nous décrivons un langage minimal qui capture la sémantique des structures de contrôle des langages data-parallèles tels que MPL de MasPar ou HyperC. en particulier, il étend le concept d'échappement du langage C scalaire, tel que le break ou continue, au cas data-parallèle. Nous en définissons une sémantique naturelle, puis nous définissons une notion d'assertion et décrivons un système de preuve de programmes par assertions selon la méthode axiomatique de Hoare. La mise en œuvre du système est illustrée par un exemple
Fichier principal
Vignette du fichier
RR1994-18.pdf (302.08 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

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

Identifiants

  • HAL Id : hal-02102484 , version 1

Citer

Luc Bougé, Gil Utard. Escape constructs in data-parallel languages: semantics and proof system. [Research Report] LIP RR-94-18, Laboratoire de l'informatique du parallélisme. 1994, 2+19p. ⟨hal-02102484⟩
16 Consultations
37 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More