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 条

[1] Verified Scalable Parallel Computing with Why3
Proust, Olivia
Loulergue, Frederic
SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2023, 2023, 14323 : 246 - 262
[2] SyDPaCC: A Framework for the Development of Verified Scalable Parallel Functional Programs
Loulergue, Frederic
Ischard, Jordan
LEVERAGING APPLICATIONS OF FORMAL METHOD, VERIFICATION AND VALIDATION: SPECIFICATION AND VERIFICATION, PT III, ISOLA 2024, 2025, 15221 : 274 - 295
[3] Combined scheduling and mapping for scalable computing with parallel tasks
Duemmler, Joerg
Rauber, Thomas
Ruenger, Gudula
SCIENTIFIC PROGRAMMING, 2012, 20 (01) : 45 - 67
[4] A scalable parallel computing SPH framework for predictions of geophysical granular flows
Yang, Edward
Bui, Ha H.
De Sterck, Hans
Nguyen, Giang D.
Bouazza, Abdelmalek
COMPUTERS AND GEOTECHNICS, 2020, 121
[5] A Parallel Random Forest Algorithm for Big Data in a Spark Cloud Computing Environment
Chen, Jianguo
Li, Kenli
Tang, Zhuo
Bilal, Kashif
Yu, Shui
Weng, Chuliang
Li, Keqin
IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS, 2017, 28 (04) : 919 - 933
[6] Parallel PSO for Efficient Neural Network Training Using GPGPU and Apache Spark in Edge Computing Sets
Capel, Manuel I.
Salguero-Hidalgo, Alberto
Holgado-Terriza, Juan A.
ALGORITHMS, 2024, 17 (09)
[7] Scalable Taxonomy Generation and Evolution on Apache Spark
Aalijah, Kanwal
Irfan, Rabia
2020 IEEE INTL CONF ON DEPENDABLE, AUTONOMIC AND SECURE COMPUTING, INTL CONF ON PERVASIVE INTELLIGENCE AND COMPUTING, INTL CONF ON CLOUD AND BIG DATA COMPUTING, INTL CONF ON CYBER SCIENCE AND TECHNOLOGY CONGRESS (DASC/PICOM/CBDCOM/CYBERSCITECH), 2020, : 634 - 639
[8] Dissecting GeoSparkSim: a scalable microscopic road network traffic simulator in Apache Spark
Yu, Jia
Fu, Zishan
Sarwat, Mohamed
DISTRIBUTED AND PARALLEL DATABASES, 2020, 38 (04) : 963 - 994
[9] Analysis of Global and Local Synchronization in Parallel Computing
Cicirelli, Franco
Giordano, Andrea
Mastroianni, Carlo
IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS, 2021, 32 (05) : 988 - 1000
[10] PRISPARK: Differential Privacy Enforcement for Big Data Computing in Apache Spark
Li, Shuailou
Wen, Yu
Xue, Tao
Wang, Zhaoyang
Wu, Yanna
Meng, Dan
2023 42ND INTERNATIONAL SYMPOSIUM ON RELIABLE DISTRIBUTED SYSTEMS, SRDS 2023, 2023, : 93 - 106

← 1 2 3 4 5 →