Formal derivation and extraction of a parallel program for the all nearest smaller values problem
Formal derivation and extraction of a parallel program for the all nearest smaller values problem
复制标题
所有最接近的较小值问题的并行程序的形式推导和提取
DOI：
10.1145/2554850.2554912
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Zhenjiang Hu
中科院分区：
文献类型：
--
作者：
F. Loulergue;Simon Robillard;J. Tesson;J. Legaux;Zhenjiang Hu
ANSV （All Nearest small Values）问题是并行编程中的一个重要问题，因为它可以用来解决多个问题，并且是其他几种并行算法的一个阶段。我们利用Coq证明助手中的批量同步并行（BSP）同态理论，构造了一个求解ANSV问题的函数并行程序。从Coq获得的批量同步并行ML程序的性能与没有软件支持的版本（笔和纸）进行了比较，并使用orlsamans Skeleton库的算法骨架实现，以及He和Huang的BSP算法的（未经证明正确的）直接实现。
The All Nearest Smaller Values (ANSV) problem is an important problem for parallel programming as it can be used to solve several problems and is one of the phases of several other parallel algorithms. We formally develop by construction a functional parallel program for solving the ANSV problem using the theory of Bulk Synchronous Parallel (BSP) homomorphisms within the Coq proof assistant. The performances of the Bulk Synchronous Parallel ML program obtained from Coq is compared to a version derived without software support (pen-and-paper) and implemented using the Orléans Skeleton Library of algorithmic skeletons, and to a (unproved correct) direct implementation of the BSP algorithm of He and Huang.
DOI：
--
发表时间：
2009
期刊：
Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL2009) POPL2009
影响因子：
--
作者：
Akimasa Morihata;Kiminori Matsuzaki;et al.
通讯作者：
et al.