Many researchers are devising algorithms for task placement in distributed systems, but few are designing the necessary mechanisms to provide the information required by those algorithms. Fundamental to these mechanisms is an accurate means for information exchange between distributed systems. The messiahs project investigated the construction of a set of mechanisms to support task placement in autonomous, heterogeneous, distributed systems. In this paper we describe the semantics of the protocols used to exchange system state information within messiahs, and develop formal models to prove that the protocols accurately propagate system description information throughout the system.
Steve J. Chapin, Eugene H. Spafford