The SyDPaCC framework supports the development of scalable parallel functional programs with Coq and helps the developers to write correct-by-construction programs with respect to specifications written as simple (and possibly very inefficient) functional programs. Parallel programs are built from specifications using verified program transformations offered by SyDPaCC. Leveraging the Coq extraction mechanism, compilable code can be obtained and executed on shared-memory or large scale distributed memory parallel machines. This paper presents the usage of SyDPaCC via an example, explains the internals of SyDPaCC and gives a tour of the program transformations provided by the framework.

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

SyDPaCC: A Framework for the Development of Verified Scalable Parallel Functional Programs

  • Frédéric Loulergue,
  • Jordan Ischard

摘要

The SyDPaCC framework supports the development of scalable parallel functional programs with Coq and helps the developers to write correct-by-construction programs with respect to specifications written as simple (and possibly very inefficient) functional programs. Parallel programs are built from specifications using verified program transformations offered by SyDPaCC. Leveraging the Coq extraction mechanism, compilable code can be obtained and executed on shared-memory or large scale distributed memory parallel machines. This paper presents the usage of SyDPaCC via an example, explains the internals of SyDPaCC and gives a tour of the program transformations provided by the framework.