DocumentCode
3322007
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
fYear
2009
fDate
18-20 Feb. 2009
Firstpage
44
Lastpage
51
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Parallel, Distributed and Network-based Processing, 2009 17th Euromicro International Conference on
Conference_Location
Weimar
ISSN
1066-6192
Print_ISBN
978-0-7695-3544-9
Type
conf
DOI
10.1109/PDP.2009.49
Filename
4912914
Link To Document