Etude et mise en oeuvre de la réécriture conditionnelle concurrente sur des machines parallèles à mémoire distribuée
Résumé
Term Rewriting is a well-known concept used in many programming languages such OBJ, as well as a fundamental mechnaism for automated deduction and formal computation. This thesis is an approach to the definition and the implementation of a conditional concurrent model on distributed memory machines. Our approach is to use the data parallelism present in term structure. Concurrent rewriting consists in the simultaneous application of several rewriting rules on the same term. First, we describe the formalisation of our model in the context of J. Meseguer's rewriting logic. To extend the model to conditional rewriting, we define a transformation from conditional to unconditional rewriting systems. We detail the implementation model and we describe the transition from the conditional concurrent rewriting abstract model to an operational model which can be implemented on distributed memory machines. The implemented model is based on asynchronous exchange of messages. We propose a concurrent garbage algorithm reclaiming unused nodes of the graph. The ReCo system implements the oerational model using MPI ou PVM message passing interface library. To validate and to experiment our implementation, different benchmarks for computing term normal forms are realised.
La réécriture de termes est un concept maintenant bien connu, qu'on retrouve à la base de langages de programmation de haut niveau tel qu'OBJ, ou encore comme mécanisme fondamental pour le calcul formel et la démonstration automatique. Cette thèse est consacrée à la définition et l'implantation d'un modèle de réécriture conditionnelle concurrent sur des machines parallèles à mémoire distribuée. Notre approche est de profiter du parallélisme de données que l'on rencontre dans les structures de termes. La réécriture concurrente consiste à appliquer simultanément plusieurs règles sur un même terme. Dans un premier temps, nous décrivons la formalisation de notre modèle de calcul dans le cadre de la logique de réécriture de J. Meseguer. Dans le but d'étendre ce modèle aux règles conditionnelles, nous définissons ensuite une transformation d'un système de réécriture conditionnelle en un système de réécriture non conditionnelle. Nous détaillons notre choix d'implantation du modèle de calcul et nous décrivons le passage du modèle abstrait de la réécriture concurrente conditionnelle à un modèle réel implantable sur des machines parallèles à mémoire distribuée. Le modèle d'implantation est basé sur la réécriture de termes représentés par des graphes particuliers appelés "jungles". Un mécanisme fondé sur des échanges asynchrones de messages permet de réaliser l'opération de réécriture. Nous proposons un algorithme de glanage concurrent opérant sur les n?uds du graphe à réduire. Le logiciel ReCo met en ?uvre directement le modèle opérationnel de la réécriture conditionnelle concurrente en utilisant le standard MPI ou la bibliothèque PVM pour le passage des messages entre processus. Pour valider et expérimenter notre modèle de calcul concurrent, différents benchmarks de calculs parallèles de formes normales de termes sont réalisés.