Keywords

1 Introduction

Distributed systems are very complex to understand and develop. There is a need to formally verify and ensure the correctness of distributed systems and algorithms. During last few years, the research in the field of formal methods has done significant work in the development of describing and analysing the complex systems in formal languages [1, 2]. In distributed systems, formal methods take an important role for ensuring the correctness of several protocols and algorithms. Formal verification is done either through model checking or theorem proving [3, 4]. Model checking is a model-oriented approach, which verifies the correctness of system automatically by traversing every possible execution path. It is expressed in terms of finite state automata that describe all possible transitions states. In this technique, for a given problem, a formal model describing its behavioural properties is developed in formal language. All the properties of models are verified. In order to verify all possible execution paths, it is required that the model must be finite. The problem may also appear when the model which is finite has considerable size. Theorem proving is the act of generating a mathematical proof for a mathematical statement to be true [3, 5, 6]. In this proving technique, system and its properties are specified in terms of mathematical logic. The verification of properties is done by discharging proof obligations generated by the system. If the proof is discharged for a statement, then it is known to be true and is said to be a theorem. The main advantage of theorem proving over model checking is that it can be used to verify the system having infinite states.

We have considered Event-B as a formal method for verification of our model. Event-B [7,8,9] is a formal technique, which is used to develop and formalize such system whose component can be modelled as discrete transition systems. It also provides refinement-based development of a complex model and has control systems within its scope. Event-B modelling can be used in various application areas like sequential programmes, concurrent programmes and distributed systems [10].

In this paper, we have developed formal model of distributed load migration mechanism using Event-B. Distributed system is a collection of autonomous systems connected by the network and they communicate with each other for the completion of common goal [11]. In this environment, the users submit the task at their sites for processing. The random arrival of tasks and their service order create the possibility that several sites may become heavily loaded and others may ideal or lightly loaded. It may degrade the performance of the whole system. Therefore, load distribution scheme is required for efficient use of resources and to enhance the performance [11,12,13]. In this paper, we have considered maximum load count value of site as the threshold value. This threshold value indicates maximum number of tasks that can be executed without affecting the performance of system. When a new task is submitted at site, the load count value of that site will be increased. When load count value of any site exceeds threshold value, then that site will become heavily loaded site. The load of this site should be transferred to idle or lightly loaded site. In order to find out low load site, heavily loaded site broadcasts load transfer request message to all sites. Site, whose load count value is lesser than threshold value, sends load reply message to sender. At any instance, lightly loaded site may receive number of load request messages from several heavily loaded sites. It will not send a reply message to all heavily loaded sites. It will send a reply only to that site first whose request for load transfer message arrived first. For ensuring ordered delivery of message, we have introduced a notion of causal order delivery [14]. The lightly loaded site will send a reply only to that site whose request for load transfer causally precedes the request from others. After receiving reply message from low load site, load from heavily loaded site will be transferred to it.

The remainder of this paper is organized as follows: Sect. 2 describes Event-B as formal method, Sect. 3 presents causal order broadcast, Sect. 4 outlines Event-B Model of causal order-based load distribution. This model consists of events like task submission event for submission of new task, enable and disable load transfer event for changing status of site when load count value increase and decrease from threshold value, broadcast and deliver event to formalize ordered delivery of load request message, reply message event, which models the sending of reply message to heavily loaded site and load reduction event to reduce load value. Finally, Sect. 5 concludes the paper.

2 Event-B

Event-B [14,15,16,17,18] is a formal technique, which captures complete system specifications on the basis of requirement and system behaviour. It can be expressed in form of states and events. It specifies the model in mathematical form. It defines mathematical structures as context and machine [19,20,21]. The context part of the model contains sets, constants and axioms, which are used to describe static properties of system. The dynamic part of the model is shown by machine part, which contains set of variables, invariants and events that modify the value of state variable when it triggers. The variables of model are constrained by invariants. The invariants of model which describe the properties of model should not be violated when an event occurs. The event contains guards which are necessary conditions for an event to trigger and list of actions. When all guards of an event become true, then set of actions written under it will be performed. The action of an event is expressed by substitution operation. It specifies how the state of system may change. The event may use local variables. The scope of that variable will be local to the event.

For ensuring correctness of the model, Event-B method requires to discharge all proof obligations generated by the model. Proof obligations serve to verify properties of the model.

There are several tools which support to write Event-B specifications. We have considered Rodin tool [22,23,24] for the development of our model. In order to discharge proof obligations generated by the model, there are various plug-ins which are provided by this tool. Event-B uses set-theoretic notations to specify the model. The syntax and detail description of Event-B notations can be found in [15].

3 Causal Order Broadcast

The formalization of causal relationship in distributed system was initiated by Lamport in [25]. Later, causal ordering of messages is proposed by Birman, Schiper and Stephenson [26]. The causal order property can be ensured by combining FIFO order and local order property [27].

FIFO order property says that if any site Si broadcasts a message Ma before broadcast another message Mb, then each receiving site delivers Ma before Mb.

Local order property says that if any site Si delivers message Ma before broadcasting message Mb, then every receiving site delivers Ma before Mb.

The causal order property says that if broadcasting of a message Ma causally precedes broadcasting of a message Mb, then delivery of message Ma at each site should be done before message Mb (Fig. 1).

Fig. 1
figure 1

Causal order broadcast

Full size image

We can say that message Ma causally precedes message Mb if send event of message Ma; send(Ma) at site Si happened before message sending event send(Mb) of message Mb at site Sj. The causality of the message can also be related with receive event of the message. A message Ma causally precedes Mb if receive event of message Ma causally precedes the broadcast of Mb. As given in Fig. 1, broadcasting of message Ma causally precedes broadcasting of Mb and each recipient site delivers Ma before Mb. Similarly, broadcasting of message Mb causally precedes broadcasting of message Mc and each recipient site delivers Mb before Mc.

4 Event-B Model of Load Distribution Mechanism

We start with the distributed system model having a set of sites. Since there is no system-wide global clock or shared memory, the information from one site to other site is exchanged through messages. At any site, new task may be submitted. The task may be process or transaction which will perform some operation (reading or writing on data objects) at that site. Therefore, submission of new task will increase the load at that site. When the load count value exceeds a certain limit known as threshold value, then the performance of the system will degrade. In order to capture maximum throughput from the system, we need to distribute load from heavily loaded site to idle site in efficient manner.

In our model, the context part contains SITE and MESSAGE as carrier set. TRANSFERSTATUS and TYPE are declared as enumerated set. The set TRANSFERSTATUS represents load transfer status of site informs of disable and enable.

Initially, load transfer status of every site is disable because every site is underloaded. When load count value exceeds threshold value, then load transfer status will be set as enable. The set TYPE has element LOAD_REQ and LOAD_REP which is used to formalize type of message as load request and load reply, respectively. The machine part consists of variables, invariants and events. The description of variables is as follows (Fig. 2):

Fig. 2
figure 2

Variables and invariants of model

Full size image
  1. (i)

    The variable load_at_site is specified as total function. It represents load count value of every site.

  2. (ii)

    The variable loadtransferstatus is a total function between site to TRANSFERSTATUS. Depending on the loadcount value, the load transfer status of every site may be either disable or enable.

  3. (iii)

    The variable threshold value is declared as natural number.

  4. (iv)

    The variable sender is specified as partial function from MESSAGE to SITE. It models the sending of message m by site s.

  5. (v)

    The variable cdeliver is declared as:

    $$cdeliver \in SITE \leftrightarrow MESSAGE$$

    The operator ↔ defines the set of relations between SITE and MESSAGE. It represents causal delivery of messages at any site.

  6. (vi)

    The variable messagesent represents the set of messages which have been sent.

  7. (vii)

    The variable messagetype maps each sent message with its type. The type of message may be load request message or load reply message.

  8. (viii)

    The variable corder models the causal relationship between messages. The mapping (mmmm) ∈ corder indicates that message m causally precedes message mm.

  9. (ix)

    The delivery order of messages at any site is shown by delorder. It is declared as relation between site to set of ordered pair of messages. The mapping ssm(mmmm) ∈ delorder indicates that at site ss message, m is delivered before message mm.

  10. (x)

    The variable replymsgsent models the sending of reply message corresponding to request message. The mapping (m1mm2) ∈ replymsgsent indicates that reply message m1 has been sent corresponding to its request message m2.

4.1 Submission of Task

The event TASK SUBMISSION is given in Fig. 3. This event model the submission of task at any site ss. Every time when this event occurs, it increases the load count value of site by one. The action act1 represents that load at site ss is incremented by one.

Fig. 3
figure 3

Task submission, enable transfer and disable transfer event

Full size image

4.2 Enabling and Disabling Load Transfer Status

The event ENABLE TRANSFER updates load transfer status of site (Fig. 3). When load count value of any site exceeds threshold value, then this event updates load transfer status of that site as enable. The guard grd2 ensures that load of site ss is greater than threshold value. The guard grd3 ensures that load transfer status of site ss is disable. The action act1 updates the load transfer status of site ss as enable.

The event DISABLE TRANSFER is given in Fig. 3. The guard grd2 ensures that load count value of site ss is less than threshold value. The action act1 set load transfer status of that site as disable.

4.3 Broadcasting and Delivery of Load Request Message

This event enables broadcasting of load request message to all sites (see Fig. 4). When the load count of any site exceeds its threshold value, then this site broadcast load request message to all sites. The purpose of the broadcasting request message is to know that which site is under loaded. The message that has not been sent is ensured by guard grd2 and grd4. The load transfer status of site ss is enable and is ensured through guard grd3. Due to the occurrence of this event, message mm will be broadcast (act2). The message mm will be added to messagesent set (act1). The action act3 set the status of message mm as load request message. In this event, we are also ensuring ordered delivery of request message at sending site. The action act4 ensures that all those messages which are sent by site ss will causally precede message mm (FIFO Order). The action act5 specifies delivery of message mm at site ss. The action act6 gives delivery order of message.

Fig. 4
figure 4

Broadcast event

Full size image

Delivery of load request message is given in Fig. 5. The guard grd3 and grd4 ensure that message mm has been sent but it is not delivered to site ss. The guard grd5 is written as

Fig. 5
figure 5

Deliver event

Full size image
$$\forall m\cdot(m \in MESSAGE \wedge (m\, \mapsto \,mm) \in corder\, \Rightarrow \,(ss\, \mapsto \,m) \in cdeliver)$$

It ensures that all messages m which causally precede message mm have already been delivered at site ss. Delivery of message mm at site ss is ensured by action act1. The action act2 makes the delivery order of messages at site ss.

4.4 Sending of Reply Message

The event REPLY is given in Fig. 6. This event models sending of load reply message (LOAD_REP) by those sites whose load count value is lesser than threshold value. The load request message mm has been received by site s is ensured by guards grd3 and grd4. Site may receive number of load request messages from several heavily loaded sites but it will send a reply only to that site whose load request message LOAD_REQ message causally precedes other requests. The guard grd5 ensures that load request message mm causally precedes all load request message msg. Therefore, site s will send load reply message m corresponding to load request message mm only. The load count value of site s is lesser than threshold value and is ensured by guard grd6. The reply message m has not been previously sent is ensured through guard grd7 and grd8. The action act1 ensures sending of message m by site s. The action act2 adds the message m to messagesent set. The action act3 set the status of message m as load reply (LOAD_REP). The action act4 makes the entry of reply message m corresponding to request message mm.

Fig. 6
figure 6

Reply event

Full size image

4.5 Load Reduction Event

This event model the load reduction from heavily loaded site (Fig. 7). The guard grd2 ensures that site ss is heavily loaded because its load count value is greater than threshold value. Guards grd3, grd4 and grd5 ensure that site ss has received the load reply message m. Receiving of reply message also indicates that there is some site whose load count value is less than threshold value. Request message mm sent by site ss is ensured through guards grd6, grd7 and grd8. The guard grd9 ensures that message m is reply message of request message mm. Due to the occurrence of this event, load count value of site ss is reduced by one (act1). After the reduction of load, it will be submitted at low load site in the form of task through TASK SUBMISSION event.

Fig. 7
figure 7

Load reduction event

Full size image

5 Conclusion

Distributed systems provide tremendous processing capacity. In order to maximize the performance of the system, good load transfer or task migration schemes are required. The random arrival order of task and its random system service may create the situation that all resources and systems may not properly be utilized. Due to uneven load distribution, few of the sites may become heavily loaded and others may be ideal. We have introduced causal order delivery of load transfer request message which ensures ordered service of load request message.

In this paper, a formal development of causal order-based load distribution mechanism is done. Formal methods are mathematical techniques to verify the correctness of system properties. We have considered Event-B as a formal method for the development of our model. In Event-B model, the properties of model are specified through invariants. These invariants should not be violated during the execution of the model. Event-B model generates proof obligations, and we need to discharge all proofs generated by it. A total of 42 proof obligations are generated by the model out of which 30 proofs are discharged automatically whilst 12 proofs are discharged interactively. In order to ensure correctness, we have added the following invariants:

$${\text{ran}}\left( {\text{cdeliver}} \right)\, ( {\text{dom}}\left( {\text{sender}} \right) \ldots \left( {\text{inv11}} \right)$$
$${\text{dom}}\left( {\text{corder}} \right)\, ( {\text{dom}}\left( {\text{sender}} \right) \ldots \left( {\text{inv12}} \right)$$
$${\text{ran}}\left( {\text{corder}} \right) \,( {\text{dom}}\left( {\text{sender}} \right) \ldots \left( {\text{inv13}} \right)$$
$$\begin{aligned} !{\text{ss}}({\text{ss}}\, \in \,{\text{SITE}}\,\& \,{\text{loadtransferstatus}}({\text{ss}})\, = \,{\text{enable}}){\text{G}}\,\,{\text{load}}\,{\text{at}}\,{\text{site}}({\text{ss}})\, > \,({\text{threshold}}\,{\text{value}}) \ldots ({\text{inv}}14) \end{aligned}$$

The invariant inv11 ensures that messages which are delivered should be a subset of messages which have been sent. Similarly, invariants inv12 and inv13 ensure that messages for which ordering is maintained (causal order) should be a subset of sent messages. The invariant inv14 ensures that if load transfer status of any site is enable, then load of that site exceeds threshold value of that site.

The invariants and proofs of model give a clear insight of model. In future, we plan to strengthen invariants and add fault-tolerance property to this model.