Title :
Formal Semantics of a Subset of the Paderborn´s BSPlib
Author :
Gava, Frdric ; Fortin, Jean
Author_Institution :
Lab. of Algorithms, Complexity & Logic (LACL), Univ. of Paris-Est, 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 indeterminism. This paper presents a formal operational semantics for a C+PUB subset language using the Coq proof assistant and a certified N-body computation as example of using this formal semantics .
Keywords :
high level languages; set theory; software libraries; C+PUB subset language; Coq proof assistant; bulk-synchronous parallel algorithm; formal operational semantics; formal semantics; Algorithm design and analysis; Concurrent computing; Distributed computing; Kernel; Laboratories; Libraries; Logic; Parallel machines; Safety; System recovery; BSP; Coq; Formal Semantics;
Conference_Titel :
Parallel and Distributed Computing, Applications and Technologies, 2008. PDCAT 2008. Ninth International Conference on
Conference_Location :
Otago
Print_ISBN :
978-0-7695-3443-5
DOI :
10.1109/PDCAT.2008.43
