Rigorous Specification of Vector Timestamp Based Load Sharing Mechanism for Distributed Systems

Distributed systems are autonomous computer nodes or sites that are interconnected by a communication network. These sites function independently without a shared memory or global clock, communicating through message exchanges. Any incoming job can be allocated to any of these independent sites within the system. This leads to a non-uniform distribution of load where some sites become highly loaded while others remain lightly loaded or idle. This scenario leads to poor utilization of resources, heightened response time and impaired system performance. This paper presents the formal specification of a load balancing protocol for distributed systems which is based on vector time-stamping of messages using the vector clock at a site. In order to add fairness to the load sharing mechanism, the request for unburdening the heavily laden site is catered to first whose request message has the least vector timestamp from among the request messages present in the request acquisition queue of the lightly loaded site. Formal methods utilise mathematical techniques to methodically detect and correct errors in the development of software in its initial phases. Event-B is a formal method used to create models of proposed algorithms. The approach used is event-driven, employing set-theoretic principles to construct models of distributed system protocols. The procedure involves creating and satisfying proof obligations to validate the correctness of a model. The article presents a rigorous analysis of the vector clock mechanism in distributed systems as well as a load distribution system which uses vector timestamped messages as the underlying message exchange protocol using Event-B.