Safe Ambients (SA) are a variant of the Ambient Calculus (AC) in which types can be used to avoid certain forms of interferences among processes called grave interferences. An abstract machine, called GcPan, for a distributed implementation of typed SA is presented and studied. Our machine improves over previous proposals for executing AC, or variants of it, mainly through a better management of special agents (the forwarders), created upon code migration to transmit messages to the target location of the migration. Well-known methods (such as reference counting and union-find) are applied in order to garbage collect forwarders, thus avoiding long - possibly distributed - chains of forwarders, as well as avoiding useless persistent forwarders. We present the proof of correctness of GcPan w.r.t. typed SA processes. We describe a distributed implementation of the abstract machine in OCaml. More broadly, this study is a contribution towards understanding issues of correctness and optimisations in implementations of distributed languages encompassing mobility. © 2007 Elsevier Inc. All rights reserved.
Hirschkoff, D., Pous, D., & Sangiorgi, D. (2007). An efficient abstract machine for Safe Ambients. Journal of Logic and Algebraic Programming, 71(2), 114–149. https://doi.org/10.1016/j.jlap.2007.02.003