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

Abstract : 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.
Document type :
Reports
Complete list of metadatas

Cited literature [16 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02102484
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 1:29:08 PM
Last modification on : Thursday, November 21, 2019 - 2:38:40 AM

File

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

Identifiers

  • HAL Id : hal-02102484, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

4

Files downloads

15