Large acohen 900x1200

Correct-by-Construction Multiprocessor Programming

Albert Cohen

Recorded 29 September 2014 in Lausanne, Vaud, Switzerland

Event: IC Colloquia - EPFL IC School Colloquia

Abstract

This talk is for people who care about program correctness and performance. About achieving both without resorting to impossible verification problems and target-specific optimizations. We will explore two complementary attempts to regain control of your favorite multi- or many-core system:

  • streaming languages (with task-parallel runtimes);
  • polyhedral compilation (for DSLs, library generation, portability).

Stream computing is often associated with regular, data-intensive applications, and more specifically with the family of cyclo-static data-flow models. The term also refers to bulk-synchronous data parallelism on SIMD and GPU architectures. Both interpretations are valid but incomplete: streams underline the formal definition of Kahn process networks, a foundation for deterministic concurrent languages and systems with a solid heritage. Stream computing is a semantical framework for parallel languages and a model for pipelined, task-parallel execution. Supporting research on parallel languages with dynamic, nested task creation and first-class streams, we propose a new lock-free algorithm for stalling and waking-up tasks in a user-space scheduler according to changes in the state of the corresponding queues. The algorithm is portable and proven correct against the C11 memory model. We show through experiments that it can serve as a keystone to efficient parallel runtime systems.

Watched 5729 times.

 Watch