Two Formal Semantics of a Subset of the Paderborn University BSPlib

PUB (Paderborn University BSPLib) is a C library supporting the development of Bulk-Synchronous Parallel (BSP) algorithms. The BSP model allows an estimation of the execution time, avoids deadlocks and non-determinism. This paper presents two formal operational semantics for a C+PUB subset language using the Coq proof assistant, one for classical BSP operations and one that emphasises high performance primitives.

• Type: Conference
• Year: 2009
• Where: PDP
• Authors: Frédéric Gava, Jean Fortin
• Keywords: BSP Model, Classical Bsp Operations, Paderborn University BSPLib, Parallel Computing, PDP 2009