A calculus of functional BSP programs with projection

Author

Loulergue, Frédéric

Author_Institution

Lab. d´´Informatique Fondalementale d´´Orleans, Univ. d´´Orleans, Orleans

fYear

2006

fDate

25-29 April 2006

Abstract

Bulk synchronous parallel ML (BSML) is an extension of the functional language Objective Caml to program bulk synchronous parallel (BSP) algorithms. It is deterministic, deadlock free and performances are good and predictable. Parallelism is expressed with a set of 4 primitives on a parallel data structure called parallel vector. These primitives are pure functional ones: they have no side-effect. It is thus possible, and we did it, to prove the correctness of BSML programs using a proof assistant like Coq. The BSlambda-calculus is an extension of the lambda-calculus which models the core semantics of BSML. Nevertheless some principles of BSML are not well captured by this calculus. This paper presents a new calculus, with a projection primitive, which provides a better model of the core semantics of BSML

Keywords

ML language; data structures; lambda calculus; parallel algorithms; parallel programming; program verification; programming language semantics; Objective Caml; bulk synchronous parallel algorithm; bulk synchronous parallel markup language; bulk synchronous parallelism; core semantics; functional BSP program; functional language; lambda calculus; parallel data structure; parallel vector; projection primitive; proof assistant; Calculus; Costs; Data structures; Libraries; Message passing; Parallel algorithms; Parallel programming; Skeleton; System recovery; Writing;

fLanguage

English

Publisher

ieee

Conference_Titel

Parallel and Distributed Processing Symposium, 2006. IPDPS 2006. 20th International

Conference_Location

Rhodes Island

Print_ISBN

1-4244-0054-6

Type

conf

DOI

10.1109/IPDPS.2006.1639552

Filename

1639552