Projet ANR-10-INTB-0205 – PAPDAS : Developpement de programmes parallèles avec des squelettes algorithmiques
Programme : Blanc international - Sciences de l'information, de la matière et de l'ingénierie : Sciences de l’information, simulation (Blanc inter SIMI 2) 2010
Année de financement : 2010
Coordinateur du projet : Monsieur Frédéric DABROWSKI (UNIVERSITE D'ORLEANS)
Partenaires : School of Information - JAPON; Laboratoire d'Informatique Fondamentale d'Orléans
Montant : 195521.0 euros
Durée : 36 mois
Résumé : La généralisation des architectures parallèles et les besoins croissants en puissance de calcul rendent toujours plus nécessaire l'application de méthodes formelles. Celles-ci permettent de spécifier précisément les propriétés des programmes parallèles et répartis et de vérifier qu'une implantation est conforme à ces spécifications formelles en utilisant des techniques mathématiques. Toutefois, en comparaison des programmes séquentiels, la complexité des programmes parallèles les rend plus sujets à erreur et difficiles à vérifier. 
Ceci motive l'utilisation de formes fortement structurées de parallélisme qui ne doivent pas seulement être munies d'abstractions qui masquent l'essentiel de la complexité des calculs parallèles mais qui doivent fournir également une méthode de développement systématique de programmes parallèles depuis des spécifications pour des programmes usuels non-triviaux.
La transformation de programmes est une méthodologie rigoureuse basée sur des fondements mathématiques pour la construction de programmes efficaces. Le calcul de programmes est un cas particulier de transformation de programmes basé sur la théorie de l'algorithmique constructive. Un programme efficace est dérivé pas-à-pas par une séquence de transformations qui préservent la sémantique et donc la correction. Sur des structures de données adéquates le calcul de programmes peut être utilisé pour écrire des programmes parallèles.
Toutefois une fois qu'une formulation efficace (et correcte par rapport à la spécification initiale) du programme est obtenue par transformations successives, le programme doit être implanté en utilisant une bibliothèque parallèle de squelettes algorithmiques qui sont la plupart du temps écrites en C++ avec des appels à une bibliothèque de communication telle que MPI. Les implantations des squelettes algorithmiques et les bibliothèques MPI ne sont pas prouvées correctes. Même si elles l'étaient, pour faire totalement confiance au programme, il faudrait pouvoir utiliser un compilateur C++ vérifié, qui n'existe pas pour l'instant. De ce fait, les bénéfices d'avoir prouvé le programme correct sont très amoindris. L'avantage est néanmoins que ces bibliothèques sont efficaces. 
Dans le projet PaPDAS nous nous intéressons à la construction d'un environnement logiciel pour faciliter le développement de programmes parallèles de façon systématique par algorithmique constructive et de soit les exécuter très efficacement, soit de les compiler avec un compilateur parallèle optimisant vérifié. 
La méthodologie du projet PaPDAS est de s'appuyer sur un modèle de parallélisme structuré. Mettre des contraintes sur le parallélisme que l'on peut trouver dans les programmes a les avantages suivants.
Une théorie de calcul de programmes peut être conçue pour servir de fondement à une méthodologie de développement systématique de programmes parallèles corrects ainsi qu'aux outils logiciels pour l'assister.
La vue globale du parallélisme fournie par le parallélisme structuré des squelettes algorithmiques offre des opportunités, absentes dans des approches moins structurées, pour l'optimisation de programmes parallèles. Nous concevrons et implanterons des bibliothèques très efficaces de squelettes algorithmiques en C++. 
Restreindre le parallélisme est également un moyen de réduire la complexité sémantique des programmes parallèles. Cela rend possible le développement d'un compilateur parallèle vérifié.
Le projet conduira : à des nouvelles théories d'algorithmique constructive et des bibliothèques Coq pour assister le développement par calcul de programmes; à des bibliothèques de squelettes algorithmiques meta-programmées en C++ très efficaces et ayant des performances prévisibles (et également partiellement vérifiées); à un compilateur vérifié en Coq pour une extension parallèle de C avec des squelettes algorithmiques.