WG211/M16Hammond

The increasing importance of parallelism has motivated the creation of better abstractions for writing parallel software, including structured parallelism using nested algorithmic skeletons. Such approaches provide high-level

 abstractions that avoid common problems, such as race conditions, and
 often allow strong cost models to be defined.
 However, choosing a
 combination of algorithmic skeletons that yields good parallel speedups for a program on
 some specific parallel architecture remains a
 difficult task. In order to achieve this, it is necessary to simultaneously
 reason both about the costs of different
 parallel structures and about the semantic equivalences between them. 

This talk presents a new type-based mechanism that

 enables strong static reasoning about these properties.  We exploit well-known
 properties of a very general recursion pattern, hylomorphisms, and give a
 denotational semantics for structured parallel processes in terms
 of these hylomorphisms. Using our approach, it is possible to determine formally
 whether it is possible to introduce a desired parallel structure into a program
 without altering its functional behaviour, and also to choose a version of that
 parallel structure that minimises some given cost model.