An Algorithm for Distributed Location
Management in Networks of Mobile Computers?
Svetlana Kryukovay, Berna Massingillz, and Beverly Sandersx
In a network supporting mobile communication devices, a mechanism to find the location of a device, wherever it may be, is needed. In this paper, we present a distributed algorithm for this purpose along with its formal specification and proof sketch. Inspired by our experiences with Wang's algorithm , one goal of this paper is to demonstrate that the process of formalization together with careful attention to abstraction and presentation can yield significant benefits in algorithm design. In this case, we obtained a more regular, general, and robust algorithm with a clearer description. An incidental contribution is a useful theorem for proving progress properties in distributed algorithms that use tokens.
1 System Description
We consider a system with a fixed network consisting of a set of nodes with unique IDs and communication links between them, plus a large number of mobile devices we will call portables. Routing1 between each pair of nodes in the fixed network is provided; knowing the identity of a node is sufficient to be able to communicate with it.
Each portable has a unique ID and is associated with a node called its home address. Given the portable's ID, it is possible to determine the home address. We will denote the home address for portable P as HA:P . At any given time, a portable may be associated with a unique node of the fixed network with which it communicates directly, typically over a wireless link. The ID of this node is
?This work was supported in part by the AFOSR under grant number AFOSR-91-0070
and in part by the University of Florida.
yTanner Research, Inc., 180 North Vinedo Ave., Pasadena, CA 91107, firstname.lastname@example.org.
zDepartment of Computer Science, California Institute of Technology, m/c 256-80, Pasadena, CA 91125, email@example.com.
xDepartment of Computer and Information Science and Engineering, University of Florida, Gainesville, FL 32611-6120, firstname.lastname@example.org.
1Routing in fixed networks has several well known solutions. See, for example, .
called the portable's location or actual address. The actual address of portable P is denoted AA:P . A message can be sent to the portable via its actual address node, which may change over time as the portable moves. Each portable is also associated with a subset of nodes called its service area. The service area models the region in which the system should be able to locate the portable.