CONFERINŢĂ
Miercuri, 05.02.2014, ora 12:00
Sala C335, Campus

Systematic Development of Correct Programs for Parallel Computing

Speaker

Pr. Frédéric Loulergue, University of Orléans

Abstract

With parallel machines being now the norm (from smart-phones to super-computers) and no longer restricted to a niche, concurrent and parallel programming has also to become widespread. To do so, it has to move to structured paradigms, in the same way sequential programming did more than forty years ago. Moreover the concern of applying formal methods arises, which allow specifications of parallel and distributed programs to be precisely stated and the conformance of an implementation to be verified using mathematical techniques. However, the complexity of parallel programs, compared to sequential ones, makes them more error-prone, difficult to verify and almost impossible to debug. Parallel programs correctness by construction is thus an essential feature. To build correct programs by constructions is not a simple task, and usually the methodologies used for this purpose are rather theoretical based on a pen-and-paper style. Such theoretical methodologies are usually based on parallel recursive structures. They are named „parallel” because their recursive nature makes them very suitable for divide-and-conquer and thus parallelism. However when one writes an application using parallel recursive structures, it is not yet implemented in parallel. A realisation of parallel recursive structures and their basic operations should be implemented using more concrete (and actually more “flat” than recursive) parallel programming languages. Moreover, a better approach could be based on software tools and formalized theories that allow a user to develop an efficient parallel application by implementing easily simple programs satisfying conditions, ideally automatically, proved. For this purpose proof assistants make the reasoning checkable by a machine, may provide some automation in reasoning, and actual programs may be extracted from developments within these proof assistants. This talk will present an effort for providing a framework based on the Coq proof assistant for the systematic development of correct programs for parallel computing.