Title :
Two Formal Semantics of a Subset of the Paderborn University BSPlib
Author :
Gava, Frédéric ; Fortin, Jean
Author_Institution :
Lab. of Algorithms, Complexity & Logic, Univ. of Paris-East, Paris
Abstract :
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.
Keywords :
C language; parallel algorithms; programming language semantics; C library; Coq proof assistant; Paderborn University BSPlib; bulk-synchronous parallel algorithms; formal semantics; subset language; Algorithm design and analysis; Kernel; Laboratories; Libraries; Logic; Parallel algorithms; Parallel machines; Parallel programming; Safety; System recovery; Formal Semantics - Coq - BSP;
Conference_Titel :
Parallel, Distributed and Network-based Processing, 2009 17th Euromicro International Conference on
Conference_Location :
Weimar
Print_ISBN :
978-0-7695-3544-9
DOI :
10.1109/PDP.2009.49
