Verified Scalable Parallel Computing with Why3
Olivia Proust (LMV), Fr\'ed\'eric Loulergue (LMV)
TL;DR
This paper formalizes and verifies the correctness of a parallel computing library, BSML, in OCaml using Why3, demonstrating its scalability and correctness through formal proofs and a small application.
Contribution
It introduces a formalization of BSML primitives in WhyML and verifies the correctness of its standard library and a sample application.
Findings
Formalization of BSML primitives in WhyML
Proof of correctness for BSML standard library
Verified small BSML application
Abstract
BSML is a pure functional library for the multi-paradigm language OCaml. BSML embodies the principles of the Bulk Synchronous Parallel (BSP) model, a model of scalable parallel computing. We propose a formalization of BSML primitives with WhyML, the specification language of Why3 and specify and prove the correctness of most of the BSML standard library. Finally, we develop and verify the correctness of a small BSML application.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsParallel Computing and Optimization Techniques · Distributed and Parallel Computing Systems · Graph Theory and Algorithms