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.