Une bibliothèque certifiée de programmes fonctionnels BSP
Bulk-Synchronous Parallel ML ou BSML est un langage fonctionnel pour la programmation d'algorithmes BSP, un modèle qui permet la portabilité des programmes tout en offrant une prévision réaliste de leurs performances sur une grande variété d'architectures. BSML est basé sur une extension du langage ML par des opérations parallèles sur une structure de données appelée vecteur parallèle. Nous présentons ici le développement d'une bibliothèque de programmes BSML certifiée par l'assistant de preuves Coq. Cette bibliothèque pourra être utilisée pour le développement d'algorithmes BSP certifiés. Ce travail est un exemple de l'adéquation des logiques d'ordre supérieur au processus de certification et de correction d'applications parallèles.
The Bulk-Synchronous Parallel ML (BSML) is a functional language for BSP programming, a model of computing which allows parallel programs to be ported to a wide range of architectures. It is based on an extension of the ML language by parallel operations on a parallel data structure called parallel vector, which is given by intention. We present the certification of a library of BSML programs with the Coq proof assistant. This library could be used for the development of certified BSP algorithms. This development is an example of the usefulness of higher-order logic in the process of software certification of parallel applications.
F.GAVA
bibliothèque, certification, preuve, fonctionnel, Coq, BSP.
library, certification, proof, functional, Coq, BSP.
Français
|
