Causality for debugging mobile agents

Mobile agents, i.e. pieces of programs that can be sent around networks of computers, appear more and more frequently on the Internet. These programs may be seen as an enrichment of traditional distributed computing, and structuring applications using mobile agents is destined to become the de facto way of constructing distributed systems in the near future. Since mobile agents may carry communication links with them as they move across the network, they create very dynamic interconnection structures that can be extremely complex to analyse. In this paper we study an example of a system based on the mobile agent principle, written in the Facile programming language. We propose a Structural Operational Semantics (SOS) for Facile, giving a proved transition system that records encodings of the derivation trees of transitions in their labels. This information enables us to easily recover non-interleaving semantics for Facile by looking only at the labels of transitions. We use the new semantics to debug an agent based system. This example is a scaled down version of a system demonstrated at the European IT Conference Exhibition in Brussels, 1995. We also adopt our causal semantics to analyse the specification of a prefetch pipeline processor.