A Fault-Tolerant Directory Service for Mobile Agents based on Forwarding Pointers

Abstract

A reliable communication layer is an essential component of a mobile agent
system. We present a new fault-tolerant directory service for mobile agents,
which can be used to route messages reliably to them, even in the presence of
failures of intermediary nodes between senders and receivers. The directory
service, based on a technique of
forwarding pointers, introduces some redundancy in order to ensure resilience
to stopping failures of nodes containing forwarding pointers; in addition, it
avoids cyclic routing of messages, and it supports a technique to collapse
chains of pointers that allows direct communication between agents. We have
formalised the algorithm and derived a fully mechanical proof of its
correctness using the proof assistant Coq; we report on our experience of
designing the algorithm and deriving its proof of correctness. The complete
source code of the proof is made available from the WWW.