Home

rapport

1. ici p soit de niveau strictement sup rieur aux missions ici p et b de sa continuation mais que le poids des missions d une r plication toujours p et b dans l exemple soit sup rieur aux poids des r ceptions p et a Dans l exemple on met un niveau b inf rieur celui de a et le terme est typable Ce typage est puissant mais son inference est NP compl te Preuve tablie par Alain Darte et Romain Demangeon Une autre d marche expos e dans DHS08 consiste v rifier l existence d un bon ordre dynamiquement c est dire au cours de l ex cution 1 3 3 V rification l ex cution de la bonne r duction d un terme annot De mani re statique on essaie de typer un processus dans le syst me DS06 En cas d chec comme dans le terme a b b a o les missions sont n cessairement aux m mes niveaux que les r plications parentes au lieu de rejeter le terme au typage il est d cor d une assertion sp cifiant la supposition faite L exemple devient la la gt b b b b gt aa Cette supposition est ensuite v rifi e l ex cution pour conserver la terminaison du processus ici puisque les deux assertions sont contradictoires toute ex cution m nera une incoh rence Il est n cessaire de modifier la s mantique du r calcul pour nos processus annot s Les m me r gles sont conserv es mais chaque processus s accompagne maintenant d un ordre partiel sur les canaux repr sentant les suppo
2. Cette solution n est possible que parce que les r gions constituent une partition des noms Les tapes pour r aliser ces regroupements et en v rifier la coh rence sont les sui vantes Initialement on cr e une tiquette de type g n rique pour chaque variable Ensuite on parcourt le terme Pour chaque canal rencontr on pr cise son tiquette et v rifie la compatibilit avec ses usages pr c dents Si on inf re que deux canaux ont le m me type alors on les fait pointer vers la m me tiquette et on inf re que leur ar guments potentiels sont de m me type on s appelle r cursivement sur leurs r gions d arguments A la fin l ensemble des variables qui pointent vers une m me tiquette correspond une classe d quivalence pour la relation avoir le m me usage en tant que nom 2 2 2 Allocation de niveau Une fois ces r gions constitu es il faut les hi rarchiser en suivant les principes expos s dans la partie 1 2 une communication sur un canal donn ne doit lib rer que des missions des canaux de niveau inf rieur On cr e un graphe de domination de la mani re d taill e en 1 2 1 on met une ar te entre la r gion d une r plication et les r gions de toutes les missions de sa continua tion On cherche ensuite les composantes fortement connexes de ce graphe si chaque ar te est seule dans sa composante alors le terme est typable On associe comme ni veau son num ro dans l ordre topologique a
3. s par d autres processus qu on appelle leur continuation dans l ensemble des processus en train de s executer Les communications ont lieu sur des canaux repr sent s par un nom sur lequel il est possible d couter ou d mettre un message Ces messages sont des n uplets de noms de canaux Si a est un nom de canal et u un message l envoi de u sur le canal a est not a u La r ception d un message sur un canal a n cessite de lier une certaine variable x afin de pouvoir faire r f rence au futur message re u dans la continuation elle est not e a x Lors d une communication la substitution des variables li es x de la r ception par le message u de l mission dans la continuation C de la r ception est not Clu x Le processus constitu d une action coute ou mission suivie d une continua tion T est not A T Les continuations et les programmes sont aussi appel s les fermes du r calcul Un terme form de l ensemble de processus P Q R est not P Q R afin de d noter les ex cutions parall les Pour comprendre prenons un programme simple si on re oit le message constitu du canal x sur le canal a alors on renvoie le message sur les canaux a et b et on coute sur x pour recevoir le message m Ce programme est not a x a x b x x m L ex cution d un terme est une succession de communications entre processus vou lant mettre et recevoir sur un m me canal Lorsqu un processus comm
4. a p b a u b v dire que a et b sont identiques n est pas suffisant car u et v doivent aussi tre regroup s Nous profiterons de ce calcul pour v rifier simultan ment que les processus pou vant tre repr sent s par la m me variable li e ont le m me nombre d arguments et pour v rifier le type des arguments afin d viter par exemple le terme a p b a b v o p est susceptible d mettre deux canaux de nature diff rente a qui est z roadique des messages vides sont mis dessus et b qui est monadique des messages singleton sont mis dessus 13 Limite de la d marche et solutions apport es 1 3 1 Un syst me de types trop contraignant L analyse expos e la partie 1 2 est correcte mais parfois pas assez subtile Le terme p a b a p a b b Pu v u 1 termine car il consomme un p et un a et lib re un p et un b Pourtant la pr sence d une mission sur p sous la r plication sur p va faire chouer le typage Cet exemple est la sch matisation simplifi e de la structure de simple table dont on se couramment en r calcul Il faut donc chercher un moyen de ne pas le rejeter 1 3 2 Evolution possible du contr le statique de la terminaison Concevoir des syst mes de types les plus permissifs possibles tout en conservant la preuve de la terminaison est l objet de la th se de Romain Demangeon mon encadrant Une premi re id e fonctionnant pour 1 est de ne plus imposer que la r plication
5. module se base sur la biblioth que ocamilgraph d velopp e par JC Filliatre Univ Orsay 2 3 2 Augmentation des possibilit s du logiciel Le code existant donnait l ensemble des processus un pas de calcul d un terme fourni Il fallait donc en d duire une fonction qui poursuive le calcul jusqu sa fin Pour viter l explosion du nombre de termes il a aussi fallu liminer les redondances en utilisant une structure d ensemble Il y a ici un gros travail autour de l galit de processus et de couple processus graphe de contr le qui ne fut pas l objet d tude durant ce stage 2 3 3 Mutation des termes Les variables li es nous posent probl me pour r aliser notre graphe Pourtant une restriction qui n est pas sous une r plication peut tr s bien a conversion pr s tre consid r e comme une variable libre de plus Le terme a x vc P se transforme en vc a x P etc Avant chaque tape de calcul nous allons donc sortir les restrictions pour les in t grer l environnement des variables libres Comme nous travaillons en indices de De Bruijn et que les lieurs sont d plac s il faut que les indices changent convena blement C est la fonction low_subst qui code la transformation Elle fait d cro tre les indices des variables libres du nombre de restrictions qu il y avait et change les in dices des variables li es en des num ros sup rieurs au nombre de variables libres afin de repr senter l i
6. pas de renommage Par exemple l ex cution de 2 est 10 70 O 0 10 70 vO v0 C est pourquoi c est la solution qu impl mente l outil dont je suis parti N anmoins sous cette forme le nom d un canal d pend de sa position La trans formation de u c x a x est 0 8 1 1 0 Pour rappel le 8 pour d signer u repr sente que nous consid rons que u est introduit par la neuvi me restriction pr c dant le terme Il est comme l indice de toutes les variables libres arbitraires seul importe qu il soit unique et coh rent tout moment On voit qu ici a est repr sent la fois par 1 et 0 et que 1 repr sente la fois c et a Il faut donc des fonctions qui maintiennent la coh rence des termes lors de leur analyse et a fortiori de leur r criture Par exemple r aliser une communication supprime le lieur de la r ception ce qui impose de diminuer tous les indices dans sa continuation tout en substituant les oc currences des variables li es par leurs valeurs 4 P 4 12 Q low_all P 12 0 Q low_all diminue tout les indices non nul de 1 Nous reviendrons rapidement sur ces manipulations lors de la pr sentation de l op ration de strip 2 3 3 2 12 D coupage g n rique du code Partir de quelque chose de d j impl ment qu il fallait adapter fut grandement simplifi par la modularit du code ma disposition Hormis quelques modifications satellites je n ai eu qu coder l algorithme d
7. probl me de la correction se d coupe en plusieurs sous probl mes plus sp ci fiques Certaines applications doivent par exemple s ex cuter en un temps fini il s agit de la propri t de terminaison C est la propri t que nous allons tudier Dans le mod le de programmation concurrente que nous avons choisi ce pro bl me est ind cidable Une solution est d imposer aux programmes des r gles trop exigeantes afin d assurer leur terminaison certains programmes terminants vont donc tre in vitablement rejet s quelle que soit la finesse de nos r gles Le but de ce stage tait de se documenter sur les diff rentes propri t s pouvant assurer la terminaison puis d impl menter un v rificateur automatique de ces pro pri t s Ce v rificateur permet par exemple de v rifier que les proc d s propos s pour transformer un programme s quentiel en un programme concurrent conservent la ter minaison Dans ce rapport la premi re partie d finira d abord le formalisme de calcul utilis puis expliquera les propri t s sur lesquelles s appuyer pour garantir la terminaison avant d exposer les raffinements de ces principes auxquels je me suis int ress La seconde partie se concentrera sur mon travail en d crivant l interpr teur dont je suis parti et la mani re dont j ai cod le v rificateur de terminaison 1 x calcul et typage Pour raisonner sur les programmes il faut un formalisme ad quat qui mod lise le comport
8. Stage de L3 Terminaison en r calcul Pierre Boutillier sous la direction de S bastien Briais et Romain Demangeon au sein de l quipe PLUME du LIP de l ENS Lyon 16 Juin 28 Juillet 2008 Introduction Lorsque qu un programme est garant de la s curit de personnes il est crucial de garantir qu il est correct d avoir une preuve de correction Formellement un programme est correct si son ex cution respecte sa s mantique c est dire v rifie une formule ma th matique donn e entre ses entr es et ses sorties Aujourd hui les demandes en calcul explosent Pour y r pondre les programmes sont crits pour s x cuter sur plusieurs calculateurs travaillant en parall le On parle de calcul concurrent Or le parall lisme ajoute un grand degr de complexit aux preuves de correction En effet la dur e n cessaire pour r aliser une op ration l mentaire d pend d nor mement de param tres nature intrins que de l op ration encombrement du r seau tat de la m moire nature et disponibilit du processeur Deux op rations faites en parall le ne vont donc pas finir dans un ordre d termin Les op rations qui leur succ dent vont donc commencer dans un ordre al atoire l ordre des op rations ap pel le flot de calcul varie donc suivant les ex cutions Ceci donne lieu une certaine forme d ind terminisme il faut alors v rifier la s mantique pour toutes les ex cutions possibles Le
9. a b 0 b fa lt b a 0 a 0 b lt a b 0 a fb lt a b 0 b f a lt b a 0 O0 CCO a fb lt a b 0 a lt b a 0 b a lt b a 0 0 cycled_ execution Importance des usages Cas sans probl me gt type p a b a bl p lt u v gt p O 2 1 u 2 v 1 Arriv e du probl me gt type p a b a bl p lt u v gt v u p O0O 2 2 u 2 v 2 Exemple de calcul o restriction r plication cr e des noms gt calc la c b lt c gt b x b y x vyl a Calculus a fTc b lt c gt 0 b x b y x y lt x y 0 a 0 fc b lt c gt 0 a c b lt c gt 0 b x b y x y lt x y 0 0 0O a fc b lt c gt 0 b y ci y lt ci y 0 O0 Conclusion Bilan Mon v rificateur de type fonctionne mais il n est certainement pas r utilisable par d autres en l tat En effet le code fourni et produit n est pas comment et il n existe pas de manuel d utilisation De plus certains exemples ont une r ponse trange s re 11 ment due un bug Ce stage a n anmoins t tr s enrichissant pour moi Il m a permis de bien comprendre le r calcul et plus g n ralement d appr hender la fois les modes de raisonnement pour prouver la terminaison et leur mise en oeuvre concr te Enfin j ai d couvert la difficult que j avais r diger et ai b n fici de no
10. a laiss de c t jusqu ici un op rateur important du r calcul l op rateur de restriction Jusque l garantir l unicit de l usage d un canal n tait pas possible Or quand un serveur renvoie une r ponse il faut que ce soit le client qui a pos la question qui la re oive et non un autre qui attend encore sa r ponse Cela est r alis par l interm diaire de l op rateur de restriction Le client cr e un canal secret qu il donne au serveur pour qu il lui r ponde Cette op ration est not e vc si c est un nom restreint Les restrictions ajoutent des canaux frais au cours du calcul Par cons quent l en vironnement change dynamiquement Pour le typage DS06 les canaux restreints sont consid r s comme les autres canaux Il n en est pas de m me pour le syst me de DHS08 o une r gle sp cifique aux variables restreintes doit tre rajout e S il existe un processus de la forme la vc alors le niveau de a doit tre stric tement sup rieur au niveau de c Les placer au m me niveau puis ajouter avant une mission sur c a gt c compromet la correction de l analyse de typage Un processus tel que p a b a vc p b c b0 Zlu v ul m ne une divergence en se rappelant r cursivement sur un nom qu il vient de cr er Ce terme ne peut tre typ l aide de l analyse que nous avons impl ment e mais les extensions de cette analyse auxquelles nous avons r fl chi durant le stage risquerai
11. duit par exemple de la mani re suivante la Blb 1b E d a b a b 2 10 Eld a eld la b 6 a l c d 61b ele d a 6lbldl8 amp ld eld bleleld ta blblol c d cld eld eleld On dispose alors d un exemple de terme qui ne termine pas sous la forme deux processus se r pondant infiniment lab bala labl balb labllbala 12 Le premier syst me de types de DS06 L objectif du typage est d obtenir un ordre multi ensemble sur les canaux qui va d cro tre strictement avec un pas de calcul La terminaison sera ainsi garantie L id e de DS06 est d associer des niveaux aux canaux de telle mani re qu une r plication sur un canal ne contienne dans sa continuation que des canaux de niveau strictement inf rieur Par exemple le terme la b b b c b admet pour type a 3 b 2 c 1 Son ex cution termine car son poids d cro t avec les transitions Le vecteur nombre d mission de poids 3 nombre d mission de poids 2 nombre d mission de poids 1 suit l volution 1 1 0 0 3 1 0 0 7 Dans cette sous partie nous verrons en 1 2 1 comment inf rer des niveaux ad quats pour les canaux Mais il faut se m fier car du fait des passages de messages un canal peut d signer ou tre d sign par deux noms diff rents Conna tre quel canal peut instancier quelle variable li e est n cessaire pour typer correctement un terme Le terme p x y x y pl
12. ement effectif du calcul et permette d crire des propri t s Dans le cadre du calcul distribu c est le r calcul qui est utilis L explication de son fonctionnement sera l objet du d but de cette partie Pour garantir la terminaison nous nous appuyons sur un syst me de types Le principe d un syst me de type pour la propri t P est d tablir une liste de r gles afin d associer inductivement une expression appel type un programme Si le m canisme aboutit alors le programme est dit bien typ Les r gles sont telles qu un pro gramme bien typ v rifie la propri t P Pour la terminaison cette m thode a t utilis e avec succ s pour le calcul mo d le du calcul s quentiel o des r sultats puissant ont t obtenus par exemple l aide de la r alisabilit Le cas du calcul concurrent est l objet des tudes actuelles dont celles men es par mes encadrants L usage des syst mes de types ne se limite pas garantir la terminaison Il existe par exemple des syst mes de types qui garantissent l quit entre clients d un serveur ou qui assurent l utilisateur la coh rence de son programme et en facilite le d bug gage 1 1 S mantique op rationnelle du r calcul A la base du r calcul se trouve la notion de communication Un programme est un ensemble d l ments appel s processus Ces l ments cherchent recevoir ou d livrer un message et s ils y parviennent ils sont substitu
13. ent de l accepter car elles introduiraient une annotation telle que le a gt c vu plus haut ce qui conduirait la construction d une cha ne infinie Une bonne prise en compte des restrictions dans l analyse de type est donc n cessaire pour garantir la terminaison 2 Impl mentation 2 1 Fonctionnement d un interpr teur Mon impl mentation s appuie sur un interpr teur d velopp par S bastien Briais dans le cadre de sa th se C est un outil originalement adapt au spi calcul qui est un mod le d riv du r calcul pour les communications s curis es Cette partie d taille deux sp cificit s de cet interpr teur qui sont la cl d une im pl mentation simplifi e et efficace d un interpr teur de r calcul 2 1 1 Indices de De Bruijn Les d finitions originelles de mod les de langages de programmation comme le calcul ou le r calcul ne permettent pas de d crire les termes de fa on canonique Par exemple les termes a x c x et a y c y d signent le m me processus celui qui renvoie sur le canal c un argument re u sur le canal a On consid re ainsi les termes modulo amp conversion c est dire renommage des variables li es De plus la r duction rend parfois obligatoire un tel renommage Ainsi le terme a x b y c x aly doit avant d tre r duit se r crire en a x b z c x aly pour que b z c y soit correct on obtiendrait sinon b y c y alors que les y sont distincts De plus
14. iff rents doivent tre bien distingu s avoir le m me type et avoir le m me type simple Deux canaux ont le m me type simple quand ils transportent la m me chose Par exemple dans amp c b d c dO a et b sont tous les deux des canaux transportant un nom de canal ne transportant rien Mais aucun moment l un et l autre ne sont en concurrence pour instancier une r ception Les niveaux de deux canaux de m me type simple sont ind pendants Deux canaux sont de m me type quand ils ont le m me usage Dans le terme alc alb a x P b et c sont de m me type car ils sont en concurrence pour rem placer x dans P Cette notion implique d avoir le m me type simple mais deux canaux de m me type doivent tout moment avoir le m me niveau Inf rer le type va revenir pour nous regrouper les noms de m me usage dans une m me r gion qui contiendra en outre une tiquette sp cifiant le type simple de ces membres Mat riellement on appelle tiquette une valeur crite en m moire qui d finit la structure d un canal Par exemple Canal ne transportant rien Canal transportant les canaux de type pointeur vers cette r gion Un type est donn par un pointeur vers une tiquette tre du m me type revient pointer vers la m me tiquette Par souci d efficacit nous utilisons des l ments qui sp cifient leur r gion plut t que la structure naturelle de r gion donnant les l ments qu elle contient
15. inf rence pour le typage et les nouvelles r gles atomiques de la s mantique L analyse syntaxique et l ex cution du nouvel in terpr teur s en sont d duits de mani re transparente Concr tement il existe plusieurs d finitions du r calcul tr s l g rement diff rentes Suivant que l on autorise un seul ou plusieurs canaux tre transport par un canal ou encore que l on parle de spi calcul ou m me de calcul symbolique les r gles de s mantique ne sont pas exactement les m mes S bastien Briais a cod un parseur re connaissant toutes ces variantes et un foncteur qui d duit des r gles donn es en entr e l interpr teur de ce calcul Il m a donc suffit d crire les r gles de la s mantique de DHS08 et de modifier le parseur pour qu il comprenne les assertions afin obtenir un interpr teur ad quat Le typage et la biblioth que de gestion d ordre taient quand m me r aliser par ailleurs En r alit le calcul o les messages sont des n uplet de canaux et non un canal n tait pas impl ment L ajouter repr senta mon premier travail 2 2 L inf rence du syst me DS06 Comme nous l avons vu en 1 2 l impl mentation du syst me de types se d coupe en deux parties dont nous tudierons successivement la mise en oeuvre 2 2 1 Concept de r gion pour repr senter les canaux substituables Lors de l inf rence des types en suivant les r gles pr sent es en 1 2 2 deux niveaux de similarit d
16. mbreux conseils et explications pour y rem dier Pistes futures Nous avons dit en 1 3 2 qu il est trop r ducteur de dominer les missions par la premi re r ception d une r plication Raisonner sur toutes les r ceptions situ es entre la r plication et la premi re mission qui la suit est parfois n cessaire pour typer un terme Pour une r plication P donn e prenons R le multi ensemble des r ceptions de P pr c dant la premi re mission de P si P lai x1 a2 x2 ax x b1 y1 C alors R a et E le multi ensemble des missions de P Imposer que tous les l ments de R E dominent chacun des l ments de E R est une approximation inf rable en temps polynomial du cas pr c dant Il est apparu durant le stage avec l tude de 1 en particulier qu il serait pertinent de l impl menter D autre part la s mantique de DHS08 mod lise mal le calcul distribu car elle contient un ordre que tout les processus doivent conna tre Il faudrait donc rechercher comment mettre en oeuvre cette s mantique de mani re r ellement distribu e Cela reviendrait ce que les processus s changent leurs connaissances partielles du graphe lors de leurs communications et que cela suffise v rifier la coh rence de l ensemble D terminer quelles sont les informations que doit poss der un processus pour d tecter les incoh rence qu il g n re est la cl pour r soudre ce probl me R f rences DHS08 R Demange
17. nsertion des restrictions en fin de liste des variables libres 2 4 Exemples On reprend ici tous les exemples rencontr s au fur et mesure de ce rapport pour illustrer comment r agit mon outil face eux Les commandes sont les suivantes type tente de typer le terme donn et renvoie les niveaux des canaux En cas d chec il rajoute les assertions ad quates calc type le terme puis r alise le calcul Il renvoie tous les termes atteignables en une communication en s parant les ensembles par une ligne de tirets Il marque qu il y sa une incoh rence dans les assertions si c est la cause de son arr t Canal aux usages incompatibles gt type a lt a gt This term can t be typed Exemple de structure de canal sur un terme sans probl me gt type a x l a lt c gt a 0 _a c a Communication sur un canal gt calc a x a lt c gt Calculus a x 0 a lt c gt 0 Exemple de terme typable avec r plication gt type la bl b cl a a 2 b 1 c 0 Calcul montrant le fonctionnement des r plications 25 cale 14 7bIAb El Ta 10 Calculus Class UT LLC 1 F amp 40 COCHON ee 0 LL BLECEO 1 09 CECEO a b 0 c 0 b c 0 0 Exemple du terme non terminant canonique gt type la bl b al a a 1 b 1 Calcul et arr t grace la s mantique tendue gt calc la bl b al a Calculus a b lt
18. on D Hirschkoff and D Sangiorgi Static and dynamic typing for the termination of mobile processes to appear in Proc IFIP TCS 08 2008 DS06 Y Deng and D Sangiorgi Ensuring Termination by Typability Information and Computation 204 7 1045 1082 2006 MNR96 Alberto Marchetti Spaccamela Umberto Nanni and Hans Rohnert Main taining a topological order under edge insertions Information Processing Letters 59 53 58 1996 Remerciement Je remercie l quipe PLUME pour l environnement de stage d tendu qu elle m a offert Je remercie vivement mes encadrants pour leur disponibilit de tous les instants Surtout je remercie Daniel Hirschkoff et Aurelien Pardon pour leur infinie patience et leur consid ration lors de la r daction du rapport sans laquelle je n aurais jamais produit ce que vous avez lu 12
19. r plication et restriction donnent lieu la cr ation de noms a va a la vcjc ala gt va la vc c a va a a vci c la vc c a la vc jc va G vc2 c2 la vc c a a 2 L encore recourir des noms frais et l a conversion est n cessaire pour faire un calcul correct Afin de r pondre ces exigences une solution connue sous le nom de convention de Barendregt est d impl menter un g n rateur de noms et de r crire les termes chaque transition de telle mani re que tous les noms li s aient des critures distinctes Cette tape est trop lourde elle augmente le temps d execution et fait exploser l espace requis pour g rer les noms Un moyen plus efficace d N De Bruijn est de d signer un nom par le nombre de lieurs les restrictions et les arguments des r ceptions qu il faut traverser pour atteindre sa definition a x vy r y se traduit en 0 7 1 0 on suppose que les va riables libres proviennent de restrictions pr fixes au terme que l on omet en toute rigueur il faudrait donc crire v0 v 1 0 La repr sentation d un terme sous cette forme est unique et non quivoque La conservation des noms sous forme de cha ne de caract re pour la reconnaissance lors du parsing puis le stockage des types des termes sont faits par le maintien d une liste des lieurs travers s jusqu au point courant La r plication d un terme en indice de De Bru jn ne n cessite
20. sitions faites ant rieurement dans le calcul Cet ordre est stock sous forme d un graphe Une tape de calcul modi fie en d finitive un processus et son graphe en un processus et le graphe augment des nouvelles suppositions faites ou L si une incoh rence dans les assertions est trouv e Si P P alors a lt B P G r 4 mo KOTA cheana jele L sinon Dans le cas de 1 le terme devient p a b a p gt plp a b b pla b a qui est ex cut jusqu ce qu on obtienne p a b a p gt plp a b b p gt plp a b b o la tentative d insertion dans l ordre de p gt p choue DHS08 donne la preuve que la version annot e d un terme calcul gr ce la nou velle s mantique n a pas d ex cution divergente L arr t sera caus par la fin du calcul ou son interruption car deux assertions contradictoires seront simultan ment n ces saires Ce syst me d annotations permet en r alit d encoder le syst me DS06 On pour rait ne pas mettre de niveau aux canaux puis pour chaque mission crire les assertions qu elle implique pour qu il n y ai pas de divergence Le syst me d crit ici est donc au moins aussi expressif que le syst me de 1 2 N anmoins cet encodage accro t inuti lement la taille des graphes de niveaux puisqu il augmente le nombre d assertions L ex cution ralentirai sans accepter plus de termes terminants 1 4 Les restrictions Afin de clarifier la pr sentation on
21. ssoci puisque l algorithme de recherche de composante fortement connexe donne directement un ordre topologique s il est appliqu un graphe sans circuit 2 3 Adaptation des termes et mise en oeuvre de la s mantique anno t e d crite en 1 3 3 2 3 1 S mantique modifi e et maintien d ordres On d fini des r gles de s mantique pour le t calcul qui transforment un proces sus en un autre processus Pour garantir l arr t nous les avons toff es et nous de vons transformer un processus des assertions et des informations de hi rarchie en un processus et des informations de hi rarchie mises jour ou L si une incoh rence est trouv e Pour ce faire il faut maintenir chaque tape du calcul un graphe sans circuit de hi rarchisation des canaux Par ailleurs nous voulons qu il n existe pas de cha ne de r duction infinie Pour v rifier cela il ne suffit pas de d rouler une ex cution possible du calcul Pour tre s r que nous ne pouvons pas trouver de chemin ne terminant pas il nous faut ex cu ter toutes les transitions possibles chaque tape puis regarder toutes les transitions possibles depuis chacune d elles Pour ne pas faire exploser le co t du calcul il nous fallait donc une impl menta tion fonctionnelle des graphes contenant des fonctions efficaces de maintien d ordre l insertion d ar tes Cette insertion d une assertion dans un ordre en maintenant sa coh rence est tir de MNR96 Notre
22. u v lu u u illustre ce danger En oubliant que x peut tre u et y v on typerait un terme qui devient lu v lu u qui ne termine pas Nous regarderons donc en 1 2 2 comment reconna tre les canaux jouant le m me r le 1 2 1 Allocation de niveaux Pour inf rer les niveaux des canaux on cr e un graphe de domination Ses sommets sont les canaux et une ar te relie a b si une mission sur b est r alis e la suite d une r plication sur a Par exemple le terme a b b c d c d a pour graphe de domination S il existe un tri topologique sur ce graphe alors le terme est typable et donc ter mine Ce tri topologique induit une num rotation des canaux que l on appelle leur niveau C 1 2 2 Reconnaissance de la structure des canaux Sans passage de nom c est dire si tous les canaux ne transportaient rien asso cier un niveau un canal sous les hypoth ses de la partie 1 2 1 suffit garantir qu il s arr tera Quand il y a concurrence pour la r ception d un message comme par exemple dans pla p b p x o a et b peuvent tous deux remplacer x il faut consid rer a b et ce x comme potentiellement quivalents lors du typage et leur donner le m me niveau Un parcours du processus afin de faire ce regroupement va donc devoir pr c der l allocation de niveaux Le regroupement des types doit se propager r cursivement aux arguments poten tiels des canaux impliqu s Par exemple dans le terme p
23. unique il lib re sa continuation Voici un exemple d une ex cution concernant cinq processus b y P a x Q atu R b v SIT by P Qlu x l R b u SIT Plu yl Qlu al RISIT Cette ex cution n est pas unique car le terme originel aurait pu d abord effectuer la communication sur b puis celle sur a De plus des processus en concurrence pour l mission d un message sont source de nn d terminisme Ainsi le terme a x P a u Q a v R peut se r duire en Plu x Q a v R ou Plv x a u Q R Dans le dernier cas le processus Q ne peut s ex cuter pas tant qu il n aura pas re u un message sur le canal a Ainsi d fini tout calcul termine n cessairement car la longueur d un terme d cro t strictement avec un pas de calcul deux actions sont consomm es chaque r duction Cependant afin de mod liser un serveur effectuant le m me calcul chaque re qu te d un client on ajoute au calcul un op rateur de r plication not et d fini par la x P quivaut la x P a x P Ainsi la x P repr sente une infinit de a x P Il n y a pas de concurrence pour acceder une ressource r pliqu Dans notre exemple si on ajoute une r plication la x P a u Q a v R devient la x P Plu x Q a v R puis la x P Plu x Plu x Q R Pour comprendre sur un exemple complet prenons le terme la b b b c d a b on consid re ici des messages vides les et sont omis il se r

rapport

Contents

Download Pdf Manuals

Related Search

Related Contents