DocumentCode
1854134
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
fYear
2008
fDate
1-4 Dec. 2008
Firstpage
269
Lastpage
276
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/PDCAT.2008.43
Filename
4710991
Link To Document