An efficient abstract machine for Safe Ambients

Abstract : 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
Document type :
Reports
Complete list of metadatas

Cited literature [23 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02102483
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 1:29:06 PM
Last modification on : Friday, April 19, 2019 - 1:38:14 AM

File

RR2004-63.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02102483, version 1

Collections

Citation

Daniel Hirschkoff, Damien Pous, Davide Sangiorgi. An efficient abstract machine for Safe Ambients. [Research Report] LIP RR-2004-63, Laboratoire de l'informatique du parallélisme. 2004, 2+33p. ⟨hal-02102483⟩

Share

Metrics

Record views

12

Files downloads

38