A Verified Accumulate Algorithmic Skeleton

被引：5
作者：
Loulergue, Frederic [1 ]
机构：
[1] No Arizona Univ, Sch Informat Comp & Cyber Syst, Flagstaff, AZ 86011 USA
来源：
2017 FIFTH INTERNATIONAL SYMPOSIUM ON COMPUTING AND NETWORKING (CANDAR) | 2017年
关键词：
Data parallel programming; functional programming; formal verification; interactive theorem proving; Coq; bulk synchronous parallelism; PARALLEL PROGRAMS; MODEL;
D O I：
10.1109/CANDAR.2017.108
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
This paper presents an extension of a library for the Coq interactive theorem prover that enables the development of correct functional parallel programs based on sequential program transformation and automatic parallelization using an algorithmic skeleton named accumulate. Such an algorithmic skeleton is a pattern of a parallel algorithm that is provided as a high-order function implemented in parallel. The use of this framework is illustrated with the bracket matching problem, including experiments on a parallel machine.
引用
收藏
页码：420 / 426
页数：7
相关论文
共 22 条
  • [1] Bird R.S., 1987, Logic of Programming and Calculi of Discrete Design, volume 36 of NATO ASI Series F, V36, P3
  • [2] Static Analysis of Communicating Processes Using Symbolic Transducers
    Botbol, Vincent
    Chailloux, Emmanuel
    Le Gall, Tristan
    [J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2017, 2017, 10145 : 73 - 90
  • [3] Bousdira W., 2010, Proceedings 2010 First International Conference on Networking and Computing (ICNC 2010), P191, DOI 10.1109/IC-NC.2010.57
  • [4] Parallel programming with list homomorphisms
    Cole, Murray I.
    [J]. Parallel processing letters, 1995, 5 (02) : 191 - 203
  • [5] Cole M.I., 1989, Algorithmic skeletons: Structured management of parallel computation
  • [6] Emoto Kento, 2014, Interactive Theorem Proving. 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014. Proceedings: LNCS 8558, P258, DOI 10.1007/978-3-319-08970-6_17
  • [7] Filter-embedding semiring fusion for programming with MapReduce
    Emoto, Kento
    Fischer, Sebastian
    Hu, Zhenjiang
    [J]. FORMAL ASPECTS OF COMPUTING, 2012, 24 (4-6) : 623 - 645
  • [8] Fortin J, 2010, HLPP 2010: PROCEEDINGS OF THE FOURTH INTERNATIONAL WORKSHOP ON HIGH-LEVEL PARALLEL PROGRAMMING AND APPLICATIONS, P35
  • [9] BSPlib: The BSP programming library
    Hill, JMD
    McColl, B
    Stefanescu, DC
    Goudreau, MW
    Lang, K
    Rao, SB
    Suel, T
    Tsantilas, T
    Bisseling, RH
    [J]. PARALLEL COMPUTING, 1998, 24 (14) : 1947 - 1980
  • [10] Hu Z., 1999, PARALLEL PROCESSING, V9, P335
123