Escape Constructs in Data-Parallel Languages: Semantics and Proof System
Luc Bougé, Gil Utard, Centre National de la Recherche Scientifique (CNRS), 69 - Lyon (France). Lab. de l'Informatique du Parallelisme, Ecole Normale Superieure de Lyon, 69 (France). Lab. de l'Informatique du Parallelisme, Lyon-1 Univ., 69 (France). Lab. de l'Informatique du Parallelisme, Institut Informatique et Mathematiques Appliquees de Grenoble (IMAG), 69 - Lyon (France). Lab. de l'Informatique du Parallelisme · 1994
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.