An efficient abstract machine for Safe Ambients
Résumé
Safe Ambients (SA) are a variant of the Ambient Calculus (AC) in which typescan be used to avoid certain forms of interferences among processes calledgraveinterferences.An abstract machine, calledGcPan, for a distributed implementation of typedSA is presented and studied. Our machine improves over previous proposals forexecuting AC, or variants of it, mainly through a better management of specialagents (theforwarders), created upon code migration to transmit messages tothe target location of the migration. Well-known methods (such as referencecounting and union-find) are applied in order to garbage collect forwarders,thus avoiding long – possibly distributed – chains of forwarders, as well asavoiding useless persistent forwarders.The proof of correctness ofGcPan, and a description of a distributed imple-mentation of the abstract machine in OCaml are given.Correctness is established by proving a weak bisimilarity result betweenGcPanand a previous abstract machine for SA, and then appealing to the correct-ness of the latter machine. This is simpler than comparingGcPandirectlywith SA, but it involves reasoning modulo ‘administrative reduction steps’ inboth machines and therefore standard techniques for simplifying proofs of weakbisimilarity results are not applicable.More broadly, this study is a contribution towards understanding issues ofcorrectness and optimisations in implementations of distributed languages en-compassing mobility
Le calcul des Safe Ambients (SA) est une variable du calcul des Mobile Ambients qui permet, par le truchement d’un système de types,d’ éviter certaines formes d’interférences appelées interférences graves. Nous définissons ici une machine abstraite, appelée GcPan, pour l’exécution de processus SA typée GcPan diffère de Pan, une machine abstraite introduite précédemment pour SA, par le fait qu’elle utilise des techniques classiques de programmation distribuée (comptage de références, union-find) afin d’améliorer les performances. En particulier, ces modifications permettent une meilleure gestion des agents de retransmission qui sont créées par la machine au moment o`u l’on fait migrer du code. Ces agents, dont le rôle est de faire suivre les messages vers la nouvelle destination d’un agent qui a migré ne sont jamais supprimés dans la machine Pan. Dans le contexte d’une implantation distribuée, cela peut engendrer des chaînes de retransmetteurs arbitrairement longues, et passant par plusieurs sites physiques.Au-delà de la comparaison avec la Pan,la GcPan se démarque des autres machines abstraites ayant été proposées pour l’exécution de calculs d’Ambients selon des critères de simplicité et d’efficacité. Le fait d’adopter le calcul des Safe Ambients plutôt que le calcul originel des Mobile Ambients, notamment,nous permet d’ éviter d’avoir à gérer des interférences graves. Par ailleurs, nous découplons la structuration logique déterminée par un processus et la description de la répartition des sous-processus au niveau physique. Nous présentons la preuve de correction de la machine proposée, et nous décrivons une implantation répartie que nous avons développée. La propriété de correction s’ énonce comme un résultat de bisimilarité ́faible entre la GcPan et la Pan(qui, à son tour, est correcte vis-`a-vis du calcul des Safe Ambients).
| Origine | Fichiers produits par l'(les) auteur(s) |
|---|
Loading...