Certified Parallel Programming

Funding

French Ministry of Research (National Science Funds), Young Researchers Program 2004 (project from september 2004 - september 2007).

The project

Introduction for non-specialists

If one wants to perform quickly a computation which needs a lot of computing power on a usual computer as a PC, one could use a parallel computer to increase the speed of the computation. A parallel computer can be imagined as a set of PC interconnected by a network working together to solve a problem. Each PC performs only one part of the computation. It can also communicate its partial results to other machines which need them to compute their own results. Some parallel machines are indeed built like that: they are called clusters of PC. A parallel program is a program written to run on a parallel computer.

Certifying a program it is proven mathematically that its behavior will always be as it is expected to be. The goals of this project is to produce a programming environment in which certified parallel programs can be written, proved and safely executed.

Technical goals

More technically, several subgoals will be studied to achieve the overall goal of the project:

• Proofs, using the Coq proof assistant, of programs written with the functional parallel languages we developped.
• Proof of correctness of the compilers for these languages, from source code to bytecode for parallel virtual machines and the proof of correctness of these virtual machines.
• Proofs of imperative bulk synchronous parallel programs.
• Performance prediction of the programs written with these languages.