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 条
  • [11] Hu ZJ, 2002, LECT NOTES COMPUT SC, V2305, P83
  • [12] Formal derivation of efficient parallel programs by construction of list homomorphisms
    Hu, ZJ
    Iwasaki, H
    Takechi, M
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1997, 19 (03): : 444 - 461
  • [13] A new parallel skeleton for general accumulative computations
    Iwasaki, H
    Hu, ZJ
    [J]. INTERNATIONAL JOURNAL OF PARALLEL PROGRAMMING, 2004, 32 (05) : 389 - 414
  • [14] Loulergue Fr d ric., 2014, ACM Symposium on Applied Computing (SAC), P1577, DOI [10.1145/2554850.2554912, DOI 10.1145/2554850.2554912]
  • [15] Calculating Parallel Programs in Coq Using List Homomorphisms
    Loulergue, Frederic
    Bousdira, Wadoud
    Tesson, Julien
    [J]. INTERNATIONAL JOURNAL OF PARALLEL PROGRAMMING, 2017, 45 (02) : 300 - 319
  • [16] Minsky Y, 2011, COMMUN ACM, V54, P53, DOI [10.1145/2018396.2018413, 10.1145/2030256.2038036]
  • [17] Morita K, 2007, PLDI'07: PROCEEDINGS OF THE 2007 ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, P146
  • [18] Owens S, 2009, LECT NOTES COMPUT SC, V5674, P391, DOI 10.1007/978-3-642-03359-9_27
  • [19] Pervez S, 2007, LECT NOTES COMPUT SC, V4757, P344
  • [20] A Verified Bulk Synchronous Parallel ML Heat Diffusion Simulation
    Tesson, Julien
    Loulergue, Frederic
    [J]. PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON COMPUTATIONAL SCIENCE (ICCS), 2011, 4 : 36 - 45
123