Formal Validation of Data-Parallel Languages

The development of massively parallel computing in the last two decades has initially been oriented towards the design of parallel architectures, rather than the definition of languages adapted to massive parallelism. Two main programming models have then emerged: control parallelism and data parallelism. Although the first one has reached a large audience, massive applications are still difficult to design, due to the huge number of processes involved. On the other hand, the data parallelism model seems to be a good compromise between the user's needs and the constraints of parallel architectures. In this thesis, we address the problem of formal validation for data parallel languages. The idea is to exploit the relative simplicity of this programming model to develop some methods, resembling those already in use for classical scalar languages. The first part of this work deals with a simple data parallel imperative language. We have shown that it was possible to define for this language a complete proof system, inspired from Hoare logic. This theoretical study has also be the key to define a practical methodology of proof by annotations, similar to the methodology used for scalar languages. We then worked on the Alpha language, that is a language of recurrence equations. It appeared that it was necessary to define a formal validation framework for this language, since the existing rewriting system allows only proofs of equivalence between programs. We have defined an execution model by means of an operational semantics, and a proof methodology. This methodology is based on invariants, that are refined from a translation of the program into a logical language to the final desired property.Le calcul massivement parallèle a connu durant ces deux dernières décennies un fort développement. Les efforts dans ce domaine ont d'abord surtout été orientés vers les machines, plutôt qu'à la définition de langages adaptés au parallélisme massif. Par la suite, deux principaux modèles de programmation ont émergé : le parallélisme de contrôle et le parallélisme de données. Le premier a connu un vif succès. Dans ce modèle cependant, les applications massivement parallèles s'avèrent difficiles à concevoir et peu fiables, compte tenu du grand nombre de processus envisagés. En revanche, le parallélisme de données paraît aujourd'hui être un bon compromis entre les besoins des utilisateurs et les contraintes imposées par les architectures parallèles. Dans cette thèse, nous nous sommes intéressé à la validation formelle des langages à parallélisme de données. L'idée est de tirer parti de la relative simplicité de ce modèle de programmation pour développer des méthodes semblables à celles déjà éprouvées dans le cadre des langages scalaires classiques. La première partie du travail effectué concerne un langage data-parallèle simple, de type impératif. Nous avons montré qu'il était possible de définir un système de preuve complet pour ce langage, inpiré de la logique de Hoare. L'étude théorique nous a permis en outre de définir une méthodologie pratique de preuve par annotations, semblable à celle utilisée pour les langages scalaires. Nous nous sommes ensuite tourné vers le langage d'équations récurrentes Alpha. Il s'avérait nécessaire de définir pour ce langage un cadre formel de validation, plus riche que le système de transformations existant ne permettant que des preuves par équivalence. Nous avons défini un modèle d'exécution par l'intermédiaire d'une sémantique opérationnelle, et une méthodologie de preuve. Celle-ci utilise des invariants qui sont raffinés à partir d'une traduction du programme dans un langage logique jusqu'à l'obtention de la propriété voulue