Blanc inter SIMI 2 - Blanc international - Sciences de l'information, de la matière et de l'ingénierie : Sciences de l’information, simulation

Developpement de programmes parallèles avec des squelettes algorithmiques – PAPDAS

Résumé de soumission

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.

Coordination du projet

Frédéric Dabrowski (UNIVERSITE D'ORLEANS) – frederic.dabrowski@univ-orleans.fr

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

LIFO UNIVERSITE D'ORLEANS

Aide de l'ANR 195 521 euros
Début et durée du projet scientifique : - 36 Mois

Liens utiles

Explorez notre base de projets financés

 

 

L’ANR met à disposition ses jeux de données sur les projets, cliquez ici pour en savoir plus.

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter