Colloquium
Stephen F. Siegel
University of Delaware
Friday, September 7, 2012
3147 MEB
Refreshments 2:00p.m.
Lecture 2:10 p.m.
Title: Scopes & Processes: a general concurrency model for parallel program analysis and model checking
Stephen F. Siegel
University of Delaware
Friday, September 7, 2012
3147 MEB
Refreshments 2:00p.m.
Lecture 2:10 p.m.
Title: Scopes & Processes: a general concurrency model for parallel program analysis and model checking
Abstract
The parallel computing landscape continues to evolve at breakneck speed. Currently available languages, libraries, and annotation systems for expressing parallelism include C11, CUDA, Chapel, Cilk, Co-Array Fortran, Java, MPI, OpenACC, OpenCL, OpenMP, Pthreads, Titanium, UPC, and X10, and more are on the way. This situation presents an extreme challenge for those working in analysis and verification of parallel programs: a tool or technique that focuses on only one of these languages is bound to have limited impact, and that impact may rapidly approach 0 as the targeted language fades in popularity and is replaced by the next great thing. One solution would be an intermediate representation that is both (1) general enough to be an easy target of translation from most of the languages, and (2) amenable to efficient automated verification techniques, such as model checking. In this somewhat speculative talk, I sketch an IR that attempts to meet these criteria, describe its syntax and semantics, and show how constructs from various languages can be translated into it. A prototype model checker for Chapel programs, based on this IR, will be demonstrated.
The parallel computing landscape continues to evolve at breakneck speed. Currently available languages, libraries, and annotation systems for expressing parallelism include C11, CUDA, Chapel, Cilk, Co-Array Fortran, Java, MPI, OpenACC, OpenCL, OpenMP, Pthreads, Titanium, UPC, and X10, and more are on the way. This situation presents an extreme challenge for those working in analysis and verification of parallel programs: a tool or technique that focuses on only one of these languages is bound to have limited impact, and that impact may rapidly approach 0 as the targeted language fades in popularity and is replaced by the next great thing. One solution would be an intermediate representation that is both (1) general enough to be an easy target of translation from most of the languages, and (2) amenable to efficient automated verification techniques, such as model checking. In this somewhat speculative talk, I sketch an IR that attempts to meet these criteria, describe its syntax and semantics, and show how constructs from various languages can be translated into it. A prototype model checker for Chapel programs, based on this IR, will be demonstrated.