Validation formelle des langages à parallélisme des données 

PARALELISME  DE DONNEES 

Introduction

De nombreux eorts ont ete mis en uvre dans les trois dernieres decennies pour developper des machines paralleles de plus en plus puissantes. De nombreux modeles d’execution ont ete proposes pour ces machines. La terminologie de Flynn ([32]) propose de classer ceux-ci, qu’ils concernent le calcul sequentiel ou parallele, en quatre categories, selon que les ots de Donnees et d’Instructions (contr^ole) sont Simples ou Multiples. En ce qui concerne les machines paralleles, cette classication distingue deux types d’architectures : SIMD (machines massivement paralleles de type MasPar) et MIMD (machines multiprocesseurs, reseaux de stations, etc.). L’histoire du developpement des machines et langages sequentiels montre que, a partir du modele d’execution quasi universel de Von Neumann, de nombreux modeles de programmation ont ete proposes. Ceux-ci ont evolue des langages (( bas niveau )) (du type Fortran) vers des langages davantage structures et abstraits (de Pascal aux langages de programmation logique, fonctionnels ou a ob jets). L’evolution du parallelisme atteint ce point depuis peu : les premieres machines etaient quasiment toutes (( livrees )) avec un modele de programmation di
erent, qui etait en fait un langage tres proche de l’architecture. Le besoin de concevoir des applications portables necessite pourtant la presence de modeles de programmation plus universels. Deux modeles de programmation, directement inspires des modeles d’execution MIMD et SIMD, sont apparus. D’un c^ote, l’abstraction du modele MIMD a donne naissance au modele de programmation du parallelisme de contr^ole, illustre par les CSP de Hoare [41], puis des langages comme Occam, ou des bibliotheques de communication comme PVM ou MPI. De l’autre c^ote, le modele SIMD a donne naissance au modele de programmation du parallelisme de donnees. Ces modeles se sont peu a peu detaches du modele d’execution sous-jacent. Un langage a parallelisme de donnees permettra par exemple de programmer a la fois un reseau de stations ou une matrice de processeurs. La distinction s’opere plut^ot maintenant au niveau du type d’applications et de la granularite du parallelisme : un langage a parallelisme de donnees sera plut^ot destine a programmer des applications regulieres, a grain n de parallelisme (typiquement du calcul scientique), alors que le parallelisme de contr^ole sera bien adapte a des applications a gros grain de parallelisme. En ce qui concerne le parallelisme massif, le modele du parallelisme de contr^ole para^t dicile a mettre en uvre, tant au niveau de la conception que du debogage ou de la validation. Il devient en eet rapidement tres complique de gerer des milliers de processus. En revanche, le modele du parallelisme de donnees, de par sa relative simplicite, semble actuellement prometteur. Cette these se penche sur le probleme de la validation de langages pour le parallelisme massif. Nous nous sommes donc naturellement tourne vers ce dernier modele. 1 Langages a parallelisme de donnees Le modele de programmation a parallelisme de donnees a donne naissance a une classe de langages de m^eme nom, encore appeles langages data-paral leles . Certains langages sont uniquement  a parallelisme de donnees explicite. Dans ces langages, le probleme de l’expression du parallelisme doit ^etre gere par le programmeur/utilisateur. C’est le cas de plusieurs langages derives de C, comme C [67] ou HyperC [57]. Un programme est une sequence d’instructions paralleles, qui sont soit des operations point-a-point entre ob jets paralleles, soit des operations de rearrangement. Par exemple, en C , si A, B et C sont des variables denies sur le domaine [1::N], l’instruction suivante A = B + C affecte a toutes les composantes de A les sommes respectives des composantes de B et de C. Avant d’effectuer cette instruction, l’utilisateur a d^u specier explicitement les domaines spatiaux de ses variables. L’instruction suivante A = [.+1]A quant a elle permet d’effectuer un decalage vers la gauche des composantes de A. Cette instruction est qualiee d’explicite dans le sens ou l’utilisateur specie lui-m^eme la fonction de communication. Par ailleurs, si l’on comprend la notion de parallelisme de donnees au sens large, la classe des langages qu’elle represente est tres vaste, puisqu’elle peut aller jusqu’a contenir tous les langages ou le parallelisme est implicite. Considerons par exemple le programme Fortran suivant DO 10 I=1,N A[I]=B[I]+C[I]  Ce programme peut ^etre execute en parallele avec une seule instruction s’executant a la fois sur tous les elements des tableaux concernes, m^eme si a priori les variables sont denies sur des tableaux sans notion de domaine spatial. Son (( comportement )) sera alors identique a celui du programme C precedent. Extraire le parallelisme d’un tel programme est le but de la parallelisation automatique : les compilateurs-paralleliseurs traduisent un programme sequentiel en un executable pour machines paralleles. Il s’agit de trouver le placement des calculs dans le temps (ordonnancement) et l’espace (allocation). De vastes travaux ont ete menes dans ce domaine de la parallelisation, que ce soit pour les langages imperatifs (voir par exemple [24] ou [28]), ou pour d’autres types de langages comme par exemple les langages a ot de donnees synchrones (voir par exemple [34]). Ce probleme est resolu pour certaines classes reduites de programmes (par exemple les nids de boucles parfaits des programmes de type Fortran), mais reste dicile dans des cas plus generaux. De nombreuses versions de Fortran ont ete developpees (CM Fortran, Fortran D, Vienna Fortran, etc.), proposant plus ou moins de parallelisme. Un pas vers une unication a ete franchi avec l’elaboration de la norme High Performance Fortran (HPF, [44]). Avec ce dernier langage, l’utilisateur peut lui-m^eme specier des instructions de contr^ole explicitement paralleles, avec par exemple la structure de contr^ole FORALL, et egalement le placement des donnees, avec les directives de compilation ALIGN et DISTRIBUTE. Les langages a parallelisme de donnees constituent donc un vaste ensemble, des plus (( explicites )) aux plus (( implicites )), avec de nombreuses gradations entre ces deux extr^emes. 2 Deux approches pour la validation formelle Le modele de programmation a parallelisme de contr^ole a benecie d’un eort important vers le developpement de methodes de validation formelle. La complexite des applications envisagees et indispensable une telle validation. Malgre leur relative simplicite, les langages dataparalleles ont ete peu etudies de ce point de vue. Dans cette these, nous essaierons de montrer que la validation de langages data-paralleles est du m^eme niveau de (( complexite )) que celle des langages sequentiels scalaires. Si nous laissons de c^ote les methodes de model-checking qui s’appliquent aux systemes d’etats nis, nous pouvons distinguer entre deux grandes classes de methodes de validation formelle.  L’approche transformationnelle, que nous appelerons egalement approche interne. Cette approche procede par reecritures successives des programmes, selon des regles garantissant une certaine equivalence. Programmes et specications sont donc ecrits dans le m^eme langage. La correction du programme nal est garantie par la correction des regles de reecriture et par celle de la specication initiale.  L’approche assertionnelle, que nous appelerons egalement approche externe. Cette approche utilise un langage d’assertion dierent du langage de programmation. Une methode de validation consiste a etablir un lien entre programmes et specications. Dans le cas des langages imperatifs scalaires, la balance penche clairement en faveur de la seconde approche, avec notamment la logique de Hoare [40]. Les langages fonctionnels s’averent en revanche particulierement favorables a la premiere. Des modeles comme Unity [18] tirent quant a eux parti des deux methodes. Dans le cadre de cette these, nous allons exclusivement nous interesser a l’approche externe, en l’appliquant a deux langages. Le premier est un langage imperatif, le second un langage fonctionnel. 3 Parallelisme explicite et langage imperatif Le premier langage auquel nous nous sommes interesse est un langage imperatif, ou le parallelisme de donnees est explicite. Ce langage, nomme L, est un langage (( jouet )), concu comme un noyau commun a plusieurs langages existants comme C ou MPL. Les methodes externes de validation formelle de langages de ce type ont deja fait l’ob jet de quelques travaux. Nous les passons brievement en revue 1 . Le langage Val de Clint et Narayana Une des premieres tentatives de construction d’un systeme de preuve pour un langage dataparallele fut celle de Narayana et Clint en 1983 [20, 21]. Ceux-ci utilisent le langage Val, inspire d’Actus. Actus [58] a ete deni par Perrott, dans le but de creer un langage parallele de haut niveau utilisable a la fois pour des tableaux de processeurs ou pour des processeurs vectoriels. Sa syntaxe est semblable a celle de Pascal. Les grands principes qui ont dirige la denition de ce langage sont les suivants.  La presence du parallelisme dans la syntaxe : l’utilisateur exprime lui-m^eme le parallelisme de son probleme .  La possibilite de faire varier le contexte, c’est-a-dire l’ensemble des indices pour lesquels une variable est active. 1. Outre les references donnees dans le texte, une description assez complete de ces approches peut ^etre trouvee dans la these de Utard : Semantique des langages a parallelisme de donnees. Applications a la validation et a la compilation, 1995 ([68]). Le contr^ole du parallelisme non seulement par les donnees, suivant le modele data-parallele, mais aussi de facon explicite. Clint et Narayana ont repris dans Val les principales caracteristiques d’Actus. Les ob jets de base de ce langage sont d’une part les tableaux, c’est-a-dire les variables paralleles, et les sequences d’acces, qui sont des ensembles ordonnes monotones et nis d’entiers. La sequence d’acces associee a une variable permet de determiner quels indices de cette variable vont ^etre utilises, et correspond donc au contexte d’activite de celle-ci. Il est possible de denir des sequences d’acces arbitraires, ou d’utiliser des operateurs de selection ou de decalage sur les sequences. Le contexte peut parfois ^etre determine de facon dynamique, par exemple dans une boucle ou une structure de conditionnement. Il existe donc un symbole special, #, qui designe le contexte courant (determine par la structure englobante) associe a la variable consideree. Par exemple, si x est une variable denie sur le domaine [1:5], et y une variable denie sur le domaine [6:10], l’expression booleenne x[1:5] >y[6:10] compare deux-a-deux les valeurs xi et yi+5. Le programme suivant if ( x[1:5] > y[6:10] ) then for x,y do x[#] := y[#]; mettra a jour, pour tous les indices i pour lesquels l’expression booleenne est vraie, la valeur de xi avec la valeur de yi+5 (et non yi ) : le signe # represente une valeur dynamique du contexte, mais qui reste locale a chaque variable. Clint et Narayana ont developpe pour ce langage un systeme de preuve dont il ont prouve la completude [20]. Dans ce systeme, le contexte est directement manipule par les assertions : la sequence d’acces associee a la variable x est notee x:as. La possibilite de manipuler de facons diverses les sequences d’acces dans le langage, ainsi que le fait d’associer a chaque variable un contexte specique, donnent des regles de preuve assez complexes que nous ne detaillerons pas ici. L’approche de Stewart Plus recemment, Stewart [65, 71, 66] a introduit en 1988 un langage qu’il a voulu independant de toute consideration d’implementation. Son but a ete d’isoler un ensemble de primitives necessaires pour la construction de programmes data-paralleles, et, surtout, de donner une semantique denotationnelle claire et precise pour ces primitives plut^ot que de favoriser une implementation pratique ou ecace. Le langage utilise par Stewart separe les structures de contr^ole parallele de la manipulation de contexte. Les constructions de ce langage sont les (( instructions SIMD generalisees )). Celles-ci sont composees de deux elements :  une instruction I ,  un sous-ensemble S de l’ensemble des indices des processeurs. L’instruction SIMD generalisee correspond simplement a l’application de l’instruction I sur le sousensemble S. Ce sous-ensemble peut ^etre aussi complexe que l’on veut : on le construit a partir de segments d’entiers, par union, intersection, ou restriction par une condition booleenne. L’affectation peut se faire avec ou sans communication, ce dernier cas n’etant qu’un cas particulier, nomme (( aectation SIMD localisee )). La communication s’eectue par l’intermediaire de fonctions de connexion, qui sont des fonctions de l’ensemble des indices dans lui-m^eme, construites par l’utilisateur et exprimees a l’aide de -termes. En plus de ces fonctions de communication explicites, les fonctions ANYIN et ALLIN permettent d’exprimer des OU et ET globaux sur un ensemble d’indices.

PARALLELISME  IMPLICITE ET LANGAGE EQUA  TIONNEL 

Le systeme de preuve utilise par Stewart repose sur un mecanisme de substitution generalisee (qualied substitution) : intuitivement, hE(i); a; Si ou E est une expression dependant de l’indice i et contenant eventuellement une fonction de communication, a une variable parallele et S un ensemble d’indices, represente l’ensemble des substitutions simultanees de a(j) par E(j) pour tout j 2 S. Ainsi, l’axiome de l’affectation s’ecrira fphE(i); a; Sig 8i 2 S: a(i) := E(i) fpg: La diculte ici reside dans la possibilite de traiter des expressions du type a(a(i)) ou a est un tableau, ce qui donne des regles de substitution assez compliquees. Le langage propose par Stewart possede l’avantage sur Val de presenter une semantique axiomatique beaucoup plus simple. Neanmoins, la construction du langage rend dicile la separation de la communication et de l’affectation (( locale )), et necessite par ailleurs de specier le contexte a chaque instruction. L’approche de Gabarro et Galvalda Gabarro et Galvalda [33] ont egalement propose en 1994 un langage data-parallele et une semantique axiomatique associee. La principale construction parallele de ce langage est la construction for all k do in parallel S(k) end qui signie que les S(k) doivent ^etre executes en parallele pour tout k. Cette construction se generalise en for all k : E(k) do in parallel S(k) end, qui signie que seuls les S(k) tels que l’expression booleenne E(k) est vraie seront executes. Le langage possede egalement une structure conditionnelle if E(k) then S(k) end, les structures telles que sequencement, boucles, procedures, etc. heritees des langages scalaires, et une instruction d’a
ectation x[F1(k)] := F2(k). Si F1(k) 6= k, il y a alors communication implicite. Plus speciquement, on trouve aussi une structure (( inconditionnelle )), unconditionally S end, qui permet l’execution de S sur tous les processeurs, quel que soit le contexte courant, ainsi que les fonctions count et enumerate qui renvoient respectivement le nombre des processeurs actifs et une enumeration de ceux-ci. L’originalite de Gabarro et Galvalda par rapport aux approches precedentes reside dans leur systeme de preuve. En effet, leur langage d’assertion dissocie les habituels predicats portant sur les variables du programme de l’expression de l’ensemble des processeurs actifs. Ceci permet de traiter de facon totalement separee les manipulations de contexte.