TowardsVerified Scalable Parallel Computing with Coqand Spark

被引：2

作者：

Loulergue, Frederic ^{[1
]}

Philippe, Jolan ^{[2
]}

机构：

[1] Univ Orleans, INSA CVL, LIFO, EA 4022, Orleans, France

[2] IMT Atlantique, INRIA, LS2N, CNRS,UMR 6004, Nantes, France

来源：

PROCEEDINGS OF THE 25TH ACM INTERNATIONAL WORKSHOP ON FORMAL TECHNIQUES FOR JAVA-LIKE PROGRAMS, FTFJP 2023 | 2023年

关键词：

Interactive theorem proving; Program transformation; Coq; Scala; Apache Spark; Algorithmic skeletons; Functional programming; FORMAL VERIFICATION; PROGRAMS; MODEL;

D O I：

10.1145/3605156.3606450

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

SyDPaCC (Systematic Development of programs for Parallel and Cloud Computing) is a framework for the Coq interactive theorem prover. It allows to systematically develop correct parallel programs from specifications via verified and automated program transformations. The obtained programs are scalable, i.e. able to run on numerous processors. SyDPaCC produces programs written in the multi-paradigm and functional programming language OCaml with calls to the BSML (Bulk Synchronous parallel ML) parallel programming library. In this paper we present ongoing work towards an extension of SyDPaCC to be able to produce Scala programs using Apache Spark for parallel processing.

引用

页码：11 / 17

页数：7

共 50 条

[31] MACHINES AND MODELS FOR PARALLEL COMPUTING
DENNIS, JB
INTERNATIONAL JOURNAL OF PARALLEL PROGRAMMING, 1994, 22 (01) : 47 - 77
[32] SFANC: Scalable and Flexible Architecture for Neuromorphic Computing
Xue, Jianwei
Ying, Rendong
Chen, Faquan
Liu, Peilin
IEEE TRANSACTIONS ON VERY LARGE SCALE INTEGRATION (VLSI) SYSTEMS, 2023, 31 (11) : 1826 - 1838
[33] Compass: A scalable simulator for an architecture for Cognitive Computing
Preissl, Robert
Wong, Theodore M.
Datta, Pallab
Flickner, Myron
Singh, Raghavendra
Esser, Steven K.
Risk, William P.
Simon, Horst D.
Modha, Dharmendra S.
2012 INTERNATIONAL CONFERENCE FOR HIGH PERFORMANCE COMPUTING, NETWORKING, STORAGE AND ANALYSIS (SC), 2012,
[34] A cylinder computation model for many-core parallel computing
Zhang, Nan
Duan, Zhenhua
Tian, Cong
THEORETICAL COMPUTER SCIENCE, 2013, 497 : 68 - 83
[35] A Scalable Farm Skeleton for Heterogeneous Parallel Programming
Ernsting, Steffen
Kuchen, Herbert
PARALLEL COMPUTING: ACCELERATING COMPUTATIONAL SCIENCE AND ENGINEERING (CSE), 2014, 25 : 72 - 81
[36] NORA: Scalable OWL reasoner based on NoSQL databases and Apache Spark
Benitez-Hidalgo, Antonio
Navas-Delgado, Ismael
Roldan-Garcia, Maria del Mar
SOFTWARE-PRACTICE & EXPERIENCE, 2023, 53 (12) : 2377 - 2392
[37] Scalable formal concept analysis algorithms for large datasets using Spark
Raghavendra K Chunduri
Aswani Kumar Cherukuri
Journal of Ambient Intelligence and Humanized Computing, 2019, 10 : 4283 - 4303
[38] Scalable formal concept analysis algorithms for large datasets using Spark
Chunduri, Raghavendra K.
Cherukuri, Aswani Kumar
JOURNAL OF AMBIENT INTELLIGENCE AND HUMANIZED COMPUTING, 2019, 10 (11) : 4283 - 4303
[39] An efficient and scalable SPARK preprocessing methodology for Genome Wide Association Studies
Agapito, Giuseppe
Guzzi, Pietro Hiram
Cannataro, Mario
2020 28TH EUROMICRO INTERNATIONAL CONFERENCE ON PARALLEL, DISTRIBUTED AND NETWORK-BASED PROCESSING (PDP 2020), 2020, : 369 - 375
[40] ParaCA: A Speculative Parallel Crawling Approach on Apache Spark
Li, Yuxiang
Zhang, Zhiyong
Niu, DanMei
Jing, Junchang
ALGORITHMS AND ARCHITECTURES FOR PARALLEL PROCESSING, ICA3PP 2020, PT I, 2020, 12452 : 112 - 124

← 1 2 3 4 5 →