Réunion de projet CARAML 19 février 2004 au LIFO

Présents: Frédéric Gava, Frédéric Loulergue, Xavier Leroy, Gaétan Hains, Armelle Merlin, Mostafa Bamha.

Xavier Leroy INRIA

Développements sur ocaml

• nettoyages des identificateurs pour conformité C
• changer la représentation des objets: problèmes d'unicité des v.tables (tables de noms de méthodes) qui peuvent varier même à l'intérieur d'un même programme => problèmes de marshaling d'objets. On pourra faire du marshaling pour programmes SPMD. Probablement disponible à l'été 2004.
• portage des compilateurs optimisants à l'architecture AMD 64 bits dont l'avenir paraît prometteur.
• concept et implantation de modules définis récursivement (travail de longue haleine).
• Damien Doliger est maintenant au projet Cristal et va participer aux travaux ci-dessus.

Le projet INRIA ESTIME a utilisé CamlP3L pour faire du couplage de composants de code numérique (Roberto DiCosmo et Pierre Weis).

Frédéric Loulergue et Frédéric Gava, LACL

Développements sur BSML

• Le travail continue sur BSMLlib certifiée en Coq
• BSMLlib avec E/S parallèles avec deux objectifs:
  1. garder le déterminisme en présence d'écriture concurrente et de fichiers multiples (un/plusieurs disques locaux + un disque partagé)
  2. modèle de coût vérifié expérimentalement
• Ecriture de squelettes en BSML (collab avec Zhenjian Hu, U. Tokyo)
• Discussion sur les possibilités de filtrage data-parallèle selon une syntaxe du genre (match z with d::r at 0 - > opération|| sur z)
• Exceptions en BSML: une exception levée au niveau local qu'on veut rattraper au niveau global. Exemple:
  try
   &   mkpar (function 0 -> failwith "aie" | _ -> true)
  with ...
  
  Travail de Frédéric Dabrowski.

Développements sur MSPML (Minimaly synchronous Parallel ML) adaptation de BSML à un concept de désynchronisation comme les horloges structurelles:

• Même syntaxe que BSML mais on n'utilise pas de put, qu'un get collectif. Ce get ne génère pas de barrière, on synchronise à la demande car l'exécution du get effectue une sauvegarde en environnement de comm. Cela simplifie le concept Caml-Flight. Communications primitives get-list
• GC des environnements de communication qui lui, engendre des barrières occasionnelles.
• Composition parallèle qui paritionne le réseau avec le problème de cohérence dynamique des barrières.

Application au GRID: on propose un système à deux niveaux. Chaque grappe est programmée en BSML et l'ensemble est traité par MSPML. Justification pratique: une barrière sur un système multi-sites est déraisonnable. => DPML (Departmental Metacomputing ML).

mkdpt : (int -> 'a) -> 'a dpar
applydpt : ('a -> 'b) -> 'a dpar -> 'b dpar
get (int -> int -> bool) par dpar -> 'a par dpar -> (int -> int -> 'a option) par dpar
dont le premier argument spécifie en chaque processeur ceux de qui il demande des données. On a aussi des variables globales représentant la grille complète
dm_p : (unit -> int) (combien de grappes dans la grille)
dm_bsp_p : int -> int (quelle taille pour quelle grappe).
Plus les opérations du niveau BSML dont put:
put : (int -> 'a option) par -> (int -> 'a option) par

Possibilité d'implantation avec la bibliothèque Madeleine de Bougé et al.

Mostafa Bamha LIFO (travail avec Matthieu Exbrayat LIFO)

Avancement du sous-projet PDBML (parallel data-base ML).

• Ameliorations sur la performance de requêtes complexes.
• Stage de Metin Osman au LIFO, extension grid de PDBML.

Possibilité d'exécuter une requête sur plusieurs grappes de PC. Hypothèse de bijection entre les processeurs et les disques. Service GLOBUS disponible sur chaque grappe. On va découper la requête globale en sous-requêtes pour chaque site, le résultat pouvant être ensuite déplacé d'un site à un autre.

Un fichier info.db contient toute l'information sur la répartition des tables entre grappes et entre processeurs des grappes. Un analyseur lit info.db et génère le plan d'exécution. Ce plan procède d'abord par la détermination du degré optimal de parallélisme. Ensuite le choix exact des processeurs. Le résultat de la requête est stocké sur les disques des processeurs choisis pour l'exécution.

Heuristique actuelle: une requête simple a des résultats placés sur une unique grappe (son calcul se fait sur une seule grappe). Dans le cas de requêtes complexes, on traite une opération à la fois sur une grappe donnée. Les tables intermédiaires peuvent se déplacer entre les sites mais ne sont pas découpées entre les sites.

Jusqu'à maintenant une table intermédiaire devait être complétée avant de passer à l'opération suivante. On étudie une approche plus efficace où les opérations peuvent être pipelinées. Cela devient possible si (et seulement si) le nombre de processeur optimal n'est pas maximal et laisse donc des processeurs libres pour les opérations suivantes. Tout ceci est géré par des histogrammes de taille des tables (combien de tuples ayant chaque valeur de l'attribut de jointure/ select ...).

Armelle Merlin LIFO (travail commun avec Gaétan Hains LIFO)

Mélange des formalismes CCS (algèbre de processus) et BSP

On part de CCS (O, a.P, P|Q, P+Q, P\a) et on ajoute un constructeur data-parallèle de processus qui est indexé dans le cas général par la grappe (ou sous-grappe) sur laquelle il s'exécute: un ensemble de processeurs. Règles de transition, bisimulation, forme simplifiée sans produits parallèles. Sur ces formes simplifiées qui représentent des systèmes de transition on définit une notion de coût. Le coût d'une transition représente le temps BSP d'exécution d'un processus. Les coûts sont dans un semi-anneau vectoriel avec structure à la BSP mais paramétré par le choix d'un semi-anneau scalaire (non-vectoriel). Problème: l'entrelâcement des événements parallèles doit se traduire dans les coûts. Détail difficile: composition séquentielle de ces coûts. Adaptation au contexte grid: multiples grappes. Applications à venir: protocoles grid et sécurité des droits d'accès dans un système parallèle.

Travail entre le LIFO (ENSI-Bourges) et le CEA: version multiprocesseur du système SELinux

Formalisation de SELinux (recherche US): matrice de droits d'accès + formule de logique temporelle -> model checker pour vérifier des propriétés induites par une politique d'accès (matrice). Formalisation d'une version parallèle de cela (Toinard, Courtieu, Hains), lien avec l'algèbre BSP-CCS de Merlin ci-dessus, travail en cours.