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

Botbol, Vincent ;

Chailloux, Emmanuel ;

Le Gall, Tristan .

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

Cole, Murray I. .

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

Emoto, Kento ;

Fischer, Sebastian ;

Hu, Zhenjiang .

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

Hill, JMD ;

McColl, B ;

Stefanescu, DC ;

Goudreau, MW ;

Lang, K ;

Rao, SB ;

Suel, T ;

Tsantilas, T ;

Bisseling, RH .

PARALLEL COMPUTING, 1998, 24 (14) :1947-1980

[10]

Hu Z., 1999, PARALLEL PROCESSING, V9, P335

← 1 2 3 →