A New Fully Distributed Resource Management System In this paper, we present a formal approach for the specification and the verification of a fully distributed resource reservation system. Our system is made of two parts: the launcher, which is executed by the user who wants to run a job on a set of computing nodes, and the agent, which is a daemon running on all the resources that exist in the system. Clients must have an exclusive access to the resources that are allocated for them. Under the requirement that clients have reasonable requirements, all the clients' requests are answered positively in a finite time and all the jobs are executed completely. In order to ensure the correctness of our system regarding such properties, we describe it using a Petri net available model, we express formally the desired prop- request answered erties and we perform their formal verification successfully. reserve Our algorithm relies on the service discovery tools provided by the Zeroconf protocol. Com- launch job cancel restart puting nodes declare themselves on the Zero- reserved conf bus. However, this simple discovery service launch is not sufficient to ensure that the computing running resources will not be used by several jobs at the dead same time. terminate failure detector
Modelling The Petri net model of a machine is presented on Fig. 1. A machine can be reserved job finished when it is available. It answers the client and switches into reserved mode. When the local Fig. 1. Model for handling reprocess is done, the machine switches to state source volatility with a failure finished, signals to the client that its part of the detector job is done, and then returns back to state available. There is only one available place on each resource, and this place contains only one token in the initial marking. Hence, a machine can answer positively to one client only.
A model where 2 clients issue concurrent resource allocation requests on the same set of resources is represented on Figure 2. Each client has its own reservation system. We represented 2 clients, one requesting n resources and the other m resources.
PNSE’15 – Petri Nets and Software Engineering
The cancel transition is very important here to release some resources in case of a deadlock caused by a conflict between applications occurring for instance when all the available machines are reserved but no application is able to start. Therefore, after a certain time, if no additional resources appear on the Zeroconf bus, the machines reserved for at least one application will be freed and become available for the other one.
begin1 start job0 n start job1 m get nodes0
get nodes1
answered1 n
launching job1 launch1 m Analysis We analyzed both generic and specific properties. As generic properties, we were rreesseerrvvee10 rreesseerrvvee01 interested in deadlock freeness, boundedness and soundness. The deadlock freeness ensures start0 start0 that no dead state (a state from which no tran- start1 . . . . start1 sition is fireable), except the final state (all machine machine the jobs are done), is reachable. The boundless property ensures that the number of reachable Fig. 2. Reservation system of 2 states is finite. This has been ensured by find- clients ing out that the state space of the system has been fully and successfully built in a finite time. Finally the soundness property implies three requirements: (1) option to complete, (2) proper completion, and (3) no dead transitions.
The table right below gives the execution time (in seconds) of Helena and statistical data on their state space : the number of reachable states, the number of terminal reachable states, and the number of arcs in the state space. We selected a set of 6 configurations according to their state space size. A first analysis of the state space report revealed that our model is bounded and that all transitions are executable.
Regarding specific properties, we were interested in checking the following: (1) It is never possible for a machine to be running two different applications, and (2) it is always possible to answer possibly any request (as long as the number of required resources is less than the number of the machines available in the system).
As a conclusion, the properties expected are all verified provided a few reasonable assumptions are made on the environment. First, if we assume that an infinite number of cancellations can Configurations Analysis results not infinitely postpone the begin- J M P F Time States Term. Arcs cnainngenosfurae stchhaetdaunleydsujobbmitthteedn jwobe 564 646 424 ynneoos 1353...199002 821,,,483066759,,,682703746 1,99911 1572,,,758454079,,,684901852 ewnilolubghe mscahcehdiunleesdaraenadvaeixlaebcluet.eSdeci-f 645 666 444 yyneeoss 1628405...302685 614523,,,610319314,,,134997480 1,7545391 1529170,,,031972664,,,415491028 ond, in the presence of machine failures, a scheduled job can always terminate if we assume that the pool of available machines allows it.