UNE MACHINE ABSTRAITE BSP POUR BSML

Définition et correction d’une machine abstraite

La correction d’une machine exprime une relation entre le code-source (provenant du terme de départ) avec lequel on initialise la machine, et la valeur qu’on extrait de l’état terminal. La correction d’une machine abstraite peut se traduire par : «la valeur résultante de l’exécution est la forme normale du programme source». Pour comprendre les mécanismes mis en œuvre par les instructions d’une machine abstraite et en interpréter les états intermédiaires, nous allons nous donner un formalisme générique pour le code-objet d’une machine quelconque. Pour ce faire, il nous faut expliquer ce qu’est une machine abstraite et ce que veut dire «compiler un programme fonctionnel» (et parallèle).

Définition d’une machine abstraite

Une machine abstraite est définie comme un automate déterministe dont les états décrivent la mémoire d’une pseudo-machine. Les transitions, elles, simulent l’exécution d’un programme sur cette machine abstraite.
Définition 18 (Machine abstraite [216]).
Une machine est une paire (E, →) où E est un ensemble d’états et→ un fonction de transition (fonction partielle de E × E dans E). Nous notons s′ = (→ (s)) par s → s′ si c ∈ E.
Il existe dans la littérature beaucoup de machines absraite différentes ; leur représentation varie d’une machine à une autre et d’un auteur à un autre. Toutefois, [216 ] a unifié leur présentation de la manière suivante :
1. Les instructions diffèrent d’une machine à une autre, mais pour chacune d’entre elles, le code est une liste (possiblement vide) d’instructions ;
2. Une fermeture est un morceau de code associé à un environnement (une substitution) et un environ-nement est une liste de fermetures ou de valeurs ;
3. Certaines machines utilisent une ou plusieurs piles de fermetures et de valeurs ;
4. La structure exacte des blocs varie suivant la machine considérée ; mais un bloc contient au moins toujours un morceau de code et un environnement ;
5. Un état de la machine abstraite est une liste de blocs.
La fonction de transition d’une machine abstraite est définie par cas sur le (ou les) bloc(s) courant(s) d’un état. Notons que, dans la plupart des cas, la transition ne dépend que de l’instruction de tête du code du bloc courant.
Nous ne décrirons, dans ce chapitre, qu’une seule machine abstraite : une CAM. Nous n’utilisons pas la ZAM [176], la machine abstraite de OCaml, car elle est bien trop compliquée pour notre propos. Les lecteurs intéressés peuvent, par une description formellede cette machine (et sa preuve de correction dans l’assistant de preuve Coq), se référer à [127] et à [216] pour un inventaire de machinesabstraites prouvées correctes (à la main) et une taxinomie des différentes machines abstraites existantes.
A cette définition de machine abstraite, nous devons ajouter un processus de compilation pour transformer un terme en un état d’une machine afin de démarrer l’exécution.
De manière réciproque, il faut définir une fonction de «décompilation» pour nous permettre d’extraire de l’état final le résultat de l’exécution d’un programme. Pourse faire, il nous faut définir la notion de valeur d’une machine abstraite. Nous allons voir pourquoi, le λ-calcul n’est pas un langage suffisant pour exprimer les valeurs des machines abstraites.

Retour sur les substitutions

Une fonction est transformée en un morceau de code fixe, accomplissant les actions inscrites dans son corps. Ce code reste inchangé pour toutes les invocations de la fonction au cours de l’exécution du programme. Cette fonction contient des variables qui peuvent être de deux sortes : ce sont des paramètres ou des variables libres (mais liées à l’extérieur du corps de la fonction). Les paramètres formels changent à chaque invocation de la fonction, tandis que les variables gardent la même valeur. Ceci amène à considérer les fermetures comme des objets de «bas niveau» décrivant les fonctions. Une fermeture est donc un couple composé du code de la fonction et de l’ensemble des valeurs que prennent les variables libres de la fonction.
Ce terme se réduit en(λy.((λz.z) y)). D’un point de vie sémantique, rien d’anormal. La variable iéel a bien été substituée par le terme donné en paramètre lors de l’application. Mais du point de vue de l’implantation, cela revient à dire que le code a été modifié pour créer cette nouvelle fonction, contredisant notre invariant qui stipule que le code est fixé1 pendant l’exécution (seules les valeurs de la mémoire changent). Si sur ce même exemple, nous considérons maintenant comme code-objet l’association du λ-terme représentant le code de la fonction et un environnement englobant les valeurs des variables libres de cette fonction, nous obtenons où ici, le code contient une variable libre dont la valeur est connue dans l’environnement (encore appelé substitution). Le code source d’un langage fonctionnel est bien le λ-calcul, car il exprime naturellement les fonctions. Mais ce formalisme n’est pas suffisant pour expri mer les valeurs calculées par les programmes. Les fermetures et les substitutions remédient à ce défaut.

Correction d’une machine abstraite

Nous pouvons maintenant préciser la notion de correction d’une machine abstraite puisque nous savons, d’une part, dans quel langage exprimer les valeurs d’une machine et, d’autre part, quel est le calcul censé s’appliquer sur un programme.

Définition d’une BSP-CAM

Machine abstraite CAM

Pour commencer, nous allons tout d’abord décrire la machineséquentielle : la CAM (Categoritical Abstract Machine) [76, 80]. La CAM était la machine abstraite de feu CAML . Nous n’avons pas choisi la ZAM qui est la machine abstraite de OCaml pour des raisons de simplicité. En effet, cette machine est bien plus compliquée et les difficultés de simulation qu’elle entraîne sont hors propos dans ce travail.

Transition de la CAM

A chaque instruction correspond une règle de transition particulière. Avant de détailler les règles de tran-sition, remarquons que chacune d’entre elles suppose que la tête de la pile soit d’une forme précise. Le fonctionnement des instructions de la CAM est le suivant :
• Cst : cette instruction modifie la tête de la pile en une constante;
• Op : cette instruction modifie la tête de la pile en une fermetureassociant le code op de l’opérateur et l’environnement en tête de pile.
• Fst et Snd : ces instructions sont respectivement la première et la deuxième projection des couples. Nous verrons par la suite que les environnements sont en fait des listes de fermetures stockées sous la forme d’arbres binaires3. Sous cette hypothèse, Fst remplace l’environnement par lui-même privé de sa première valeur etSnd accède à la nème valeur de l’environnement. Ces instructions apparaissent toujours dans une série d’instructions de la forme Fstn ; Snd. Leur exécution a pour effet d’accéder à la (n+ 1)ème valeur de l’environnement en tête de pile (l’environnement est détruit pour être remplacé par une valeur) ;
• Push : cette instruction a pour effet de dupliquer l’environnement courant afin que deux séries d’instructions aient chacune une copie de cet environnement (cela partage donc l’environnement courant) ;
• Swap : cette instruction a pour objet d’échanger les têtes de pilepour restaurer l’environnement courant avant d’entreprendre l’évaluation d’une autre série d’instructions ;
• Cons : construit une paire avec deux valeurs ;
• App : cette instruction s’exécute sur une paire (valeur d’une fonction ou d’un opérateur, valeur d’un argument). Elle introduit un nouveau calcul en reprenant l’exécution sur le code de la fermeture avec pour environnement courant son environnement augmenté parla valeur de l’argument. Une fois ce code entièrement exécuté, le calcul reprendra là où il avaitété laissé mais avec le résultat du calcul en tête de pile.
• Closure(C′) : cette instruction crée une fermeture associant le code C′ et l’environnement en tête de pile. Cette instruction a aussi pour effet de détruire l’environnement courant. L’instruction CloseRec fait de même mais exécute préalablementC′ (récursion) ;
• Case(C1, C2 ) : cette instruction permet de choisir l’exécution du codeC1 ou du code C2 suivant la tête de la pile et en le consommant ; de transition est dépendante de deux entiersi et p qui seront le «pid» du la CAM et le nombre de processeurs de la BSP-CAM.

De la CAM à la BSP-CAM

Dans un paradigme SPMD, le programme est identique en chaque processeur. Comme nous l’avons vu dans le chapitre 3, les programmes BSML peuvent être évaluéscomme des programmes SPMD (sémantique distribuée). Pour évaluer nos programmes BSML sur une machine abstraite BSP, nous reprenons ce principe pour définir une BSP-CAM.

Primitives parallèles

Plutôt que de donner une fonction de compilation C de nos termes dans une BSP-CAM, nous allons procéder en deux étapes. La première consiste à transformer les termes qui sont spécifiques au parallèlisme, c’est-à-dire les primitives parallèles. Ensuite la fonction de transformation sur ces termes permet d’obtenir le code parallèle. Ceci nous permet de différencier ce qui est propre à la CAM de ce qui est générique à BSML.
La figure 4.2 donne le schéma de compilation des primitives parallèles. Notons tout de suite que celles-ci sont «supprimées» afin de fournir un code générique dépendant d’opérations parallèles de plus bas niveau. Détaillons ce schéma de compilation :
• La primitive mkpar est traduite en une fonction qui attend un argument, puis crée un vecteur avec cet argument et le pid du processeur ;
• La primitve apply est traduite en une fonction à deux arguments (les vecteurs) et qui applique le premier argument au deuxième. Un vecteur est alors construit à partir du résultat du calcul local ; L’instruction Loc permet de passer du contexte global (en dehors du vecteur) au contexte local. Cette ins-truction testera aussi la validité des paramètres (pouvons-nous évaluer cette valeur localement, comme dans le cas d’un mkpar ?) ou détruira le constructeur de vecteur afin d’évaluer localement l’expression (cas d’un put ou d’un proj) ou pour un couple de vecteur (cas d’un apply). L’instruction Par construit le vecteur parallèle et fait repasser au contexte global. L’instruction Delpar correspond à l’opérateur delpar qui supprime le constructeur des vecteurs. Le test V() est défini à la figure 4.4. Celui-ci parcourt inductive-ment la valeur. Si la valeur est une fermeture, alors le test parcourt les instructions pour vérifier qu’elles ne font pas référence à des valeurs parallèles ou qu’elles ne sont pas elles-mêmes des instructions parallèles.