Parallel and Distributed Computing Applications and Technologies, International Conference on (2010)
Wuhan, Hubei China
Dec. 8, 2010 to Dec. 11, 2010
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/PDCAT.2010.86
With the current generalisation of parallel architectures arises the concern of applying formal methods to parallelism. The complexity of parallel, compared to sequential, programs makes them more error-prone and difficult to verify. Bulk Synchronous Parallelism (BSP) is a model of computation which offers a high degree of abstraction like PRAM models but yet a realistic cost model based on a structured parallelism. We propose a framework for refining a sequential specification toward a functional BSP program, the whole process being done with the help of the Coq proof assistant. To do so we define BH, a new homomorphic skeleton, which captures the essence of BSP computation in an algorithmic level, and also serves as a bridge in mapping from high level specification to low level BSP parallel programs.
Homomorphic skeleton, Parallel functional programming, Program derivation, Proof assistant
Julien Tesson, Frédéric Loulergue, Kiminori Matsuzaki, Louis Gesbert, Zhenjiang Hu, "Systematic Development of Correct Bulk Synchronous Parallel Programs", Parallel and Distributed Computing Applications and Technologies, International Conference on, vol. 00, no. , pp. 334-340, 2010, doi:10.1109/PDCAT.2010.86