An ASM-based Model for Grid Job Management
Alessandro Bianchi, Luciano Manelli, Sebastiano Pizzutilo · 2013
State Machine, ASM for short, is a powerful computational model [34], which has been successfully applied in several cases for modeling critical, complex systems, both in industry and in academia: wide discussion about ASM application is in [7]. It simulates every algorithm’s behavior through a step-by-step way: each step computes a set of updates with given transition rules. After the completion of a step, all updates are committed simultaneously. The concept of abstract state in ASM extends the usual notion of state occurring in Finite State Machines: it is an arbitrarily simple or complex structure, i.e. a collection of domains, with arbitrary functions and relations defined on them. On the other hand, rules are basically nested if-then-else clauses with a set of functions in their bodies. In each state, all conditions guarding rules are checked, that is all rules whose conditions are evaluated to true are simultaneously executed, so determining the state transition. All the parameters are stored in a set of so called locations and at each time the particular configuration of parameters values determines the current state of the ASM. The transition from one state to another is described through a set of formulas, in the form: {if conditioni then updatesi} i = 1,..,n where each conditioni (the guard of the i-th rule) is an arbitrary first-order formula, whose interpretation can be true or false, and each updatesi is a finite set of assignments f(t1,...,tn) = t whose execution is to be understood as changing the value of the function f at the given parameters ti, that leads to a new value of the parameter t. The parameters are stored in a set of locations and the configuration of parameter values at each step determines the current state of the ASM. For the unambiguous determination of a next state, it is necessary that updates are consistent. An update set is consistent if it contains no pair of updates which assign different values to the same location; otherwise, the update set is inconsistent. The concepts related to modeling monolithic systems through ASMs can be extended to distributed systems. The case of job management in Grid systems is a typical case of asynchronous distributed systems. It is distributed because its overall behavior is the composition of different, independent, remote elements, each operating on its own. It is asynchronous because all involved logical components operate and communicate concurrently, each according to its internal behavior. So, job EMSs in Grid can be modeled by a Distributed Asynchronous ASM asyncASM [7], [21]. Essentially, asyncASMs generalize simple ASMs to an arbitrary finite number of independent agents [23], each executing an ASM in its own local state. Formally, an asyncASM is given by a family of pairs (a, ASM(a)) of pairwise different agents, elements of a possibly dynamic finite set Agent, each executing its ASM, ASM(a). In this sense, each agent a executes its own program, operating 298 Informatica 37 (2013) 295–306 A. Bianchi et al. on its own states, so determining a partial view of the entire system. The relation between global and local states is supported by the reserved keyword self, used to denote the specific agent executing a rule, and to store information relevant to itself. A new agent can be introduced into the asyncASM at any time by extending the set Agent. An ASM-based process for developing complex systems is presented in [7]: it allows capturing system model requirements and refining them through intermediate models to any desired level of detail in a validated and verifiable code. In the present work, modeling and implementation activities have been carried out with the support of the coreASM framework [8], [9], [22]. It follows mathematical definition of ASMs and inherits several typical features of the ASM modeling. Its main purpose is to make ASM-based models executable. To this end, the framework includes some language constructs aimed at making easy the development, as, for instance, forAll, which allows executing all rules satisfying a given guard condition; choose, aimed at expressing non-determinism in the choice of a rule to execute when a condition is satisfied; seqblock/endseqblock are the delimiters of block, whose rules must be executed sequentially; par/endpar are the delimiters of block, whose rules must be executed concurrently; enqueue/dequeue are the operators for adding / removing elements to a queue. 4 Modeling the Grid job EMSs In order to model the job EMSs, firstly the Grid capabilities and features are informally described, then they are abstracted and formally defined, finally the asyncASM is created in the coreASM environment [8]. 4.1 Informal description of a Grid system