Diffusing mobile processes

This paper presents a diffusion-based model for the design of correct distributed systems of communicating mobile objects. It first makes a proposal for a new diffusion computation-model, based on broadcasting communications for mobile processes instead of, basically used, point-to-point communication schemes. For this model we have developed a process calculus for reconfigurable communicating systems based on mobile processes, which has broadcast as unique basic exchange mechanism, b pi-calculus introduced initially in [5,6]. We have provided a full operational semantics for this calculus and we have illustrated its expressiveness through some examples taken from complementary classes of applications (built correct exchange mechanisms for messages in reconfigurable networks, checking for inconsistencies of transactions between mobile distributed processes). We have proposed three behavioral equivalencies for reasoning about such systems, namely, barbed equivalence, step-equivalence and labeled bisimilarity. An important result [6] is that all these relations coincide, providing different ways to study the equivalence/non-equivalence of two systems and also a further refinement model for broadcasting systems. Then we use a restricted diffusion scheme for constructing correct routing functions for mobile processes in general interconnected networks. We present a new model of routing messages in ad-hoc networks that allow mobile processes to communicate without explicit knowledge of their actual location. The management of the process location is done at routing level, and we present for this new model routing functions that are proved correct and valid for any connected (reconfigurable) network. We also prove that these functions verify two important correction criteria: validity and deadlock avoidance for any network interconnection topology. We demonstrate a good trade-off between the length of resulting communication paths and the number of nodes that are to be notified for each process migration. We also provide a way to represent routing information to drastically reduce the overhead of memory space required when the routing model is implemented with a deterministic or an adaptive routing approach.