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

Abstract

(eng) 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.