Scholarlink

<p>Bulk synchronous parallelism (BSP) is a simple, yet realistic, model of scalable parallel computing. BSML is a pure functional library for the multi-paradigm language OCaml that embodies the principles of BSP. We propose a formalization of BSML primitives with WhyML, the specification language of <span>Why3</span> and specify and prove the correctness of a set of parallel functions forming a standard library. We develop and verify the correctness of small BSML applications based on transformation theorems and the correspondence of a set of sequential functions on lists with algorithmic skeletons, i.e., functions implemented in parallel and manipulating distributed lists. Leveraging the <span>Why3</span> feature generating OCaml code from WhyML code, we experiment these applications on parallel machines.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Deductively verifying functional scalable parallel programs with Why3

  • 期刊论文

  • 发表日期：

    2026年2月11日

查看全文
  • Frédéric Loulergue,
  • Olivia Proust

摘要

Bulk synchronous parallelism (BSP) is a simple, yet realistic, model of scalable parallel computing. BSML is a pure functional library for the multi-paradigm language OCaml that embodies the principles of BSP. We propose a formalization of BSML primitives with WhyML, the specification language of Why3 and specify and prove the correctness of a set of parallel functions forming a standard library. We develop and verify the correctness of small BSML applications based on transformation theorems and the correspondence of a set of sequential functions on lists with algorithmic skeletons, i.e., functions implemented in parallel and manipulating distributed lists. Leveraging the Why3 feature generating OCaml code from WhyML code, we experiment these applications on parallel machines.