Optimal Deployment of Formally Specified Distributed Systems

The performance characteristics of a distributed computer system depend, in part, on the placement of its components within the target network. For a given pattern of interactions among components, hosting decisions involve tradeoffs between local and remote communication, in the context of constraints such as the separation of components for fault-tolerance. This thesis explores the use of constraint programming for calculating optimal deployments of formally specified distributed systems. ^ Two related deployment problems are identified. The first assigns components to hosts, typically at system initialization, in order to minimize communication costs. The distributed systems are specified and proved correct using T EMPO, a formal specification language and development environment. This thesis extends the TEMPO language with deployment annotations for specifying target network characteristics and hosting constraints. An annotated system specification then is translated into a program that calculates an optimal deployment honoring the constraints. The optimization program is written in COMET, a state-of-the-art constraint programming language. Constraint programming models are developed for networks with and without bandwidth restrictions on the communication links. In both cases, the model outperforms mixed-integer programming (MIP) techniques. ^ The second deployment problem assigns data items to participating hosts in a data replication service, where the objective is to minimize the communication costs to contact a sufficient subset of data items, called a quorum. In order for the data replication service to be long-lived, the locations of the data items are dynamically reconfigurable in response to changes in the target network. The constraint programming model is applied to RAMBO, a formally specified atomic read/write shared memory service for dynamic networks. Each RAMBO participant observes its message frequencies and delays, communicates this data to the other participants, and uses it to request timely quorum reconfigurations. A new configuration is calculated by the constraint programming model, with experimental results indicating feasible response times for RAMBO networks and quorums of reasonable size.