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 [J].

Hu, ZJ ;

Iwasaki, H ;

Takechi, M .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1997, 19 (03) :444-461

[13] A new parallel skeleton for general accumulative computations [J].

Iwasaki, H ;

Hu, ZJ .

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 [J].

Loulergue, Frederic ;

Bousdira, Wadoud ;

Tesson, Julien .

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 [J].

Tesson, Julien ;

Loulergue, Frederic .

PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON COMPUTATIONAL SCIENCE (ICCS), 2011, 4 :36-45

← 1 2 3 →