Parallélisme vrai
L'objectif de la recherche en parallélisme vrai est de trouver de bons modèles pour l'implémentation du parallélisme et de fournir des méthodes d'analyse et de vérification plus fines que les méthodes désormais classiques de réduction de systèmes de transitions. En ce qui concerne ce dernier point, nous travaillons en étroite collaboration avec l'equipe vérification de systemes distribués de notre projet.
Nous avons développé depuis quelques années une nouvelle manière de traiter le problème du parallélisme vrai, fondée sur la notion de localité : l'idée est de rendre observable, dans une certaine mesure, la répartition spatiale d'un système parallèle, en nommant les sites dans lesquels se produisent des actions. Ce faisant, nous pouvons distinguer de manière très fine des systèmes dont le comportement global est similaire mais dont la structure de parallélisme est différente.
Parallélisme et ordre supérieur
Deux points principaux constituent cette recherche. Le premier concerne l'étude du parallélisme potentiel dans l'évaluation des programmes fonctionnels ainsi que l'étude de la question de l'évaluation optimale. Le second est l'étude des relations entre programmation fonctionnelle et programmation parallèle : il s'agit d'étudier l'intégration de ces deux paradigmes. Nous abordons ces questions à travers les modèles mathématiques fournis par le lambda-calcul et le pi-calcul.
L'objectif de l'étude systématique des relations entre parallélisme et calcul fonctionnel est de comprendre comment réussir une intégration entre ces deux paradigmes de calcul. En particulier, la programmation fonctionnelle offre l'avantage de mettre en oeuvre des concepts mathématiquement très bien compris, en apportant des éléments de sécurité comme l'inférence de types polymorphes. On sait que le calcul parallèle est loin d'être aussi bien maitrisé, en particulier à cause du non-déterminisme de l'évaluation, et de l'absence d'une bonne notion de type. Un premier problème est donc de déterminer ce qui survit de l'harmonie du monde fonctionnel lorsqu'on le plonge dans un univers parallèle.
Une partie de la réponse a été fournie par l'introduction d'un raffinement du lambda-calcul fondé sur l'idée de multiplicité : ie le lambda-calcul avec multiplicités. Ce calcul, tout en restant très proche du modèle fonctionnel, introduit des phénomènes nouveaux, typiques du parallélisme, comme la possibilité de blocage de l'évaluation, ou le non-déterminisme.
disclaimer - HTML
3.2 Checked
Last modified:
Mon Jul 12 99
maintened by: Silvano
Dal-Zilio
(Silvano.Dal_Zilio@sophia.inria.fr)
![[Page Theorie]](IMAGES/petit-logo-mobility-trans.gif){kind=logo}