PerTiMo: A Model of Spatial Migration with Safe Access Permissions

摘要

We introduce a process algebra with processes able to migrate between different explicit locations of a distributed environment defined by a number of spatially distinct locations. We use timing constraints to control migration and communication, and local clocks and local maximal parallelism of actions. Two processes may communicate if they are present in the same location and, in addition, they have appropriate access permissions (put or get) to communicate over a shared channel. Access permissions can be acquired or removed while moving from one location to another. Timing constraints coordinate and control both the communication between processes and migration between locations. We completely characterize those situations when a process is always guaranteed to possess safe access permissions. In this way one can design systems in which processes are not blocked (deadlocked) due to the lack of dynamically changing access permissions.