Grid is one of the most eective new paradigms in large scale distributed computing. Only recently Petri nets have been adopted as a formal modeling framework for describing the specic aspects of the Grid. In this paper we describe a Grid tool for High Energy Physics data analysis, and we show how modeling its architecture with nets-withinnets has led us to identify and solve a number of defects aecting the current implementation.
In particular, the features of Renew used to model the system are such that the
obtained model is very similar to a hypernet [
In the literature high level Petri nets have been applied to dierent contexts
related to Grid computing technologies. Most of the works in this eld focus
on the usage of Petri nets as a tool for workows specication and execution
[
The remainder of the paper is organized as follows: Section 2 introduces the basic notion of nets-within-nets we refer to, and the Renew tool. Section 3 describes the Grid architecture we are considering, while in Section 4 the modeling of the system and the bugs found thanks to the formal approach are presented. A discussion about the modeling choices used in our approach is made in Section 5. Finally, some conclusions are reported in Section 6. 2
The Nets-Within-Nets Paradigm and Renew
According to the nets-within-nets paradigm, the tokens of a Petri net can be
structured as Petri nets themselves. This idea is due to Valk (see [
In all these models a system is usually modeled as a collection of nets. One net is designated as the system net, the top level of the net hierarchy. All other nets are assigned to an initial place, a place in which they reside initially. This distribution of nets induces a hierarchy. The system evolves by moving tokens from place to place through the ring of autonomous transitions, or by synchronizing transitions between nets at dierent levels. The hierarchical structure of the model is usually static, but in some models there can be interactions between nets at dierent levels in the hierarchy which can dynamically change the hierarchy itself. For example, in hypernets a net N can be moved from a place belonging to a net A, to a place belonging to a distinct net B. The interaction between nets A and B is only possible if they are close in the hierarchy.
The development of the Renew software tool [
From a syntactical point of view the Renew constructs we used in our model are the following:
A net instance is created by a transition inscription of the form var : new netname, which means that the variable var will be assigned a new net instance of type netname.
An uplink is specied as a transition inscription :channelname (expr) . It provides a name for the channel and a variable which is used for vertical communication between nets.
A downlink has the form netexpr :channelname (expr) where netexpr is an expression that must evaluate to a net reference.
To re a transition that has a downlink, there must be an input arc labelled with a proper variable name ( netexpr for the previous downlink example), and this variable must evaluate to a net instance. The referenced net instance must provide an uplink with the same name,and it must be possible to bind the variables suitably so that the channel expressions evaluate to the same values on both sides. The parameter is bound to a variable present in one of the input arcs of the up(down)-link, and then it is bound to the parameter in the corresponding down(up)-link. Then the transitions can re simultaneously.
The exchange of (structured) tokens between nets, typical of hypernets, is possible by means of parameters. Figure 1 shows an example. The only transition enabled at the beginning is create (Figure 1(a)), which creates an empty child1 net, and a child2 net (Figure 1(b), and Figure 1(c) respectively). The dierence between using the parenthesis or not using the parenthesis in creating a new net is that, if you use them, then the transition that is being red must synchronize on the channel new() in the child net. Therefore, transition create in the system net synchronizes with transition create in the child1 net, which creates the ANet net. Afterwards, transitions exchangeNet, moveANet, receiveANet can re, moving ANet to child2.
Let us notice that in our model the exchange of tokens between the two children nets, child1 and child2, is made under the supervision of the system net. This means that the system net in some way observes the token exchange between its children. [] ANet (after)
The Application Context: Grid distributed analysis The CMS experiment at CERN produces about 2 Petabytes of data to be stored every year, and a comparable amount of simulated data is generated. Data needs to be accessed for the whole lifetime of the experiment, for reprocessing and analysis, from a worldwide community: about 3000 collaborators from 183 institutes spread over 38 countries all around the world.
The CMS computing model uses the infrastructure provided by the
Worldwide LHC Computing Grid (WLCG) Project [
In this Section we describe in detail the process of submitting jobs to the Grid through the CRAB Analysis Server. For each relevant component of the system its net representation is discussed. In addition, the bugs that have been discovered thanks to the net models are presented with the solutions that the actual code has adopted in order to solve the issues. The CRAB analysis suite was modeled using nets in a hierarchical fashion, as shown in Figure 2. A vertical line with multiplicity n, indicates the presence of n nets in the higher one (e.g.: the CRABClient net contains from 1 to N Task nets); a horizontal dashed line indicates that the linked nets are references to the same net. In our modeling we consider one client just for the purpose of simplicity. Of course, the discussed functionalities and use cases still hold when a larger number of clients
TaskRegister 1..N Task reference 1
1 Overall System
CRABClient 1 1..N Task 1..N
Job CRABServerWorker 1..N
1..N Job
SubmissionWorker 1
Job is considered, as the client server model assumes no direct interactions among the clients. In addition, for the use case that will be discussed, the server code separates properly the session of work for every task.
The OverallSystem net, which is the system net, contains three nets which respectively model the behavior of the client who is using the CRAB server (CRABClient net ), the TaskRegister component which is a thread running on the CRAB server ( TaskRegister net ), and the CRABServerWorker which is also a thread running on the server ( CRABServerWorker net ). Tasks are the objects a client creates, and deals with. They are composed of jobs, the single units of work that need to be performed. The TaskRegister component is responsible for registering tasks, i.e. creating some data structures on server disks, checking if each task has all the inputs it needs to be executed, and checking if the Grid can access the proper security credentials to execute it. The CRABServerWorker component continuously receives jobs, schedules them for execution on the Grid infrastructure, and creates a SubmissionWorker thread which monitors the lifecycle of each job on the Grid. The clients interact with the server, and can initiate some operations like: submitting jobs, killing them if needed, and asking for the results. 4.1
CRABClient, Tasks, and Jobs The rst component we are going to discuss is the CRAB client, which is modeled with the net in Figure 3. This component is what enables all the action sequences that the users can do on their Grid analyses.
The rst thing a client does is to create a new task on the client machine. The typical usage pairs a unique task with a CRAB analysis session. For this reason we assume that the tasksPool can contain a nite number of tokens. After the task has been locally created on the client machine, the client can perform a submit operation, which is of course the most important one as it starts the submission chain. The rst time a task is submitted to the server, it is also regiscrab -create task :new Task() task tasksPool task :csf(task) crab -submit (first) crab -resubmit task:getjob(j) j:crs() task task crab -clean submittedTaskPool task task task task task crab -overkill
task:ck() crab -kill task:getjob(j)
j:ck() crab -submit task:cs(jobs) :cs(jobs) crab -getoutput task:getjob(j)
j:cg() tered by the TaskRegister component. Subsequent submits are handled directly by the CRABServerWorker component. In our model the dierence between the two types of submits is modeled as two dierent transitions. In particular crab -submit(first) transition has an uplink (:csf(task) ), which means that it must be synchronized with the upper level. As a result the task reference is copied to the TaskRegister component by the Overall System net. After creation, the main operations a user can do are submit, resubmit, kill, getoutput, and clean. All these operations require an interaction with the server, but since we have focused on the submission use case, these interactions have not been explicitly modeled. For example the getOutput command is modeled as an interaction between the client and the job by means of two inscriptions. Handling all the possible interactions between the actors involved in the system would have resulted in a very big model, making it impossible to describe in this paper.
A task, see Figure 4, is a bag of jobs (the system allows to collect up to 4000 jobs into a singe task) and it is a representation that CRAB uses to perform collective actions on the Grid processes. Places notRegistered, registering, registered of the Task net contain information about the state of a task itself. These places control the enabledness of transitions crab -submitFirst , and taskRegistered, which are respectively called by the CRABClient when a job is submitted, and by the TaskRegister component when the task has been successfully registered after a submit rst operation. The submit transition is called when a notRegistered
createdJobs v x y z :new() v:new job crab -create x:new job y:new job z:new job :csf() crab -submitFirst firstSubmittedJobs taskRegistered :registered(j1,j2) j1:cs() j2:cs()
CRABClient performs a submit subsequent action. In our model both taskRegistered, and submit transitions send upward two jobs through a synchronous channel, and make the job move to the submission request state.
The net representing the state of Grid jobs and their allowed actions is reported in Figure 5. This net has been modeled combining the nite state machine reported in the CRAB ocial documentation with the information extracted directly from the portion of code devoted to the Grid job state handling. Several transitions of this net contain uplinks, and therefore have to be synchronized with some other net. Transitions with a :crs() uplink (CRAB Resubmit) are resubmit
:crs() :ck()
fastKill killrequest
:ck() :crs() aborted killsuccess killdone killrequest killfailed resubmit :crs() sub.failed cleaned created
[] :cs() submission sub.request resubmission :crs() :f() submission fail submission successful
:s() sub.success
job finished output retrieval
:cg() cleared tsk/pr expire terminated gridabort
resubmit transition enabled only if the job is in a state where a resubmit is possible, and are synchronized with the crab -resubmit transition of the CRABClient net, or the resubmit transition of the SubmissionWorker net. In the same way killings (channel :ck()), failures (channel :f()), submission (channel :s()), and output retrieving (channel :cg()), have to be synchronized with a correspondent transition in another net.
The integration of the documentation and the code with the formalism of the nets has allowed us to identify a bug in the way job states are modied. In particular, the net allows some transitions that are not actually activated by any event observed by the system (bug 1, b1). For example let us consider the unlabeled transition between the sub.success and the cleaned places in Figure 5: the latter denotes that a job has been abandoned because the user security credentials are expired and the Grid will not manage processes whose owner cannot be recognized. A malicious code interacting with the clients in place of the proper server could move jobs arbitrarily to this terminal state. The x for this bug consisted in a review of the code managing the job state automata in accordance with what is stated by the presented Job net. Also, the pre-conditions that allow a client to perform a kill request over the jobs are not granted properly (b2): jobs can be killed when they are in states where the killing is dangerous. For example, a user could run into a condition where a failed job cannot be resubmitted as the system requires to kill it. That means the job is in a deadlock, as a failed job cannot be killed on the Grid. 4.2
TaskRegister The TaskRegister component, shown on the left of Figure 6, duplicates the task and jobs structures that have been created at the client side and alters all the object attributes in order to localize them with respect to the running environment of the server, taking care also of security issues (like user credentials delegation) and les movement (check the existence of input). We modeled this cloning by means of the reference semantics : the TaskRegister component receives from the client a copy of the reference which points to the Task.
The component is able to handle more tasks simultaneously thanks to a pool of threads implementing the net of Figure 6. The rst transition that is red is submission, which is synchronized with the transition in the system net that receives the task reference from the CRABClient. Then four operations which can fail are executed on the task. These include local modication of the task with respect to the server environment, the user’s credential retrieval (also known as delegation), the setting of the server behavior according to what the credentials allow to do and, nally, the checking that the needed input les are accessible from the Grid. If the registration fails the only possible operation available is archiveTask which deletes the reference to the task from the task register component. If the user has the privileges to execute the jobs in the task, and if the inputs needed by the task are available, then a range of jobs is selected from the task and passed to the CRABServerWorker by ring the toCSW transition (again under the supervision of the system net). The modeling and the simulation of the TaskRegister net has highlighted some relevant defects and bugs. In case of failure the TaskRegister component was not able to set properly the status of the jobs in a task to fail. This macroscopic lack in the system design implied dierent side eects. The server was not able to discriminate whether to retry automatically the registration process or to give up and notify the user about the impossibility to proceed (b3). In addition, the system could not tell if the registration has been attempted previously. This implies that the client transfers the input data every time a registration failure appears, with a waste of network resources (b4). Both the defects have been solved by introducing the proper synchronization between the fail transition in the component with submission failed in the job net. Mapping the synchronization into the server code has granted that the status of the jobs is set to the correct failure state and that :init(j) loadGridData
j listMatch submit
j:s() evaluateOutcome j j j j j j j j j j j j j
j j:f() fail j:f() fail fail j:f() j j:f() fail fail the submission counters are properly incremented (being implementative details the counter is not reported in the Job net). With this modication the server becomes aware that a rst try has been executed and also network transfers are exploited more eciently. A second bug has been identied thanks to the study of the synchronization among the transitions for the client, the jobs and the TaskRegister nets. In detail, the handling of the kill commands presents some issues. If a user requires to kill some jobs while the task is being registered, the system cannot distinguish properly which jobs have to be killed and therefore it applies an over-killing strategy by halting the whole task (b5). This happens because the code performs some sort of synchronization with the Task net instead of having rendezvous with the related transitions into the lists of killing jobs.
The killing of Grid jobs is a demanding action, both in terms of network communications and in terms of coordination among the dierent services involved in a Grid. Furthermore the killing of an analysis job is a permitted but infrequent action. For these reasons the CRAB developers have decided to suppress this early job termination feature in order to avoid the bug. Now users are allowed to kill jobs only once they have been actually submitted to the Grid. 4.3
CRABServerWorker, and SubmissionWorkers In our model the result of a submit operation is that the CRABServerWorker component, shown in Figure 7, receives a structured token in the place accepted. If the submit was the rst, transition newTaskRegistered is red after the task has been registered by the TaskRegister component by means of transition toCSW, which is synchronized with transition newTaskRegistered through the overall system. If the submit is not the rst, the task has been already registered, therefore transition subsequentSubmission is red. After receiving the range of jobs, the CRABServerWorker component schedules these jobs for the execution on the Grid infrastructure. The practical eect of this component is to break the task into lists of jobs in order to improve the performance thanks to bulk interactions with the Grid middleware. The Submission Worker thread spawned by the component monitors the actual submission process of the jobs. We have modeled this fact by creating a Submission Worker net for each one of the jobs in the list. Indeed, transition triggerSubmissionWorker creates a new Submission Worker assigned to the variable sw and synchronizes it with a transition labeled init.
:acceptTR(j1,j2) newTaskRegistered j1 j2 j1 j2
j acceppted
schedule subsequentSubmission :subsequentSubmission(j1,j2) j
j
The thread is responsible both for tracking the submission to the Grid infrastructure, and for resubmitting jobs when a failure occurs. Failures can occur for dierent reasons: network communication glitches, unavailable compatible resources, etc. Some types of failures are recoverable and in those cases the Submission Worker automatically tries to resubmit the job a three times. This value can be congured in the code, but in the model we only used the actually employed value of three. If the failure persists the job is permanently marked as failed. The net shown on the right in Figure 6 is our model of the submission worker component.
The study of the synchronization between the job and the Submission Worker nets allowed us to identify another bug in the code. The submission success transition in the job net (Figure 5) synchronizes with the submit Submission Worker’s transition (right of Figure 6). This means that the CRAB Server marks the submission as successful just after the interactions with the Grid. Actually the network latencies could delay the propagation of the job failure message (b6) and, therefore, the correct rendezvous should be enacted between submission success and evaluateOutcome.
It is relevant to observe that the approach followed for the modeling of the CRAB Server submission chain is a particular case for a quite general class of Grid systems. All the Grid middlewares rely on jobs that are represented by nite state automata and that are concurrently managed by the dierent services involved in the Grid. In addition, the intermediate action of a broker like the CRAB Server is becoming a common pattern with the diusion of scientic gateways: programmatic portals that abstract the user applications from the complexities of the distributed infrastructures acting as back end.
The adoption of the nets-within-nets paradigm has provided a natural and eective way to model subtle interactions among the dierent net levels. It would have required a signicantly greater eort to discover the same problems with a at net approach. In the following subsection details about the process of deriving the models from the documentation and the code are given. 4.4
Details on the model derivation process The model was derived from the code by analyzing both the ocial documentation and the source code of the system. The Job net is directly built from the documentation. A nite state automata which describes the Job is reported explicitly. After that, simply by using pattern matching we analyzed the source code relevant for the submission use case by searching for interaction with jobs. Each source module is modeled as a net (e.g.: CRABClient, TaskRegister, CRABServerWorker etc), and the interactions with the Job nets are modeled using the Renew uplink/downlink mechanism. A modication of the status of a job in the code is modeled as a pair of synchronized transitions in the model itself: one in the job net and one in the net that models the component changing the job status.
To ensure that the model is an accurate representation of the software, we made several task submissions with the CRAB tool and monitored the status of the jobs during the evolution. The request parameters were set up so that dierent behaviours of the system are tested. For example, jobs lacking of input les, job submitted by users with expired credentials, and jobs killed before the completion of task registration process are test cases that have been considered. After that, we simulated each submission on the model, taking care that the simulation of the status of the job net was consistent with the actual job status in the system. 5
In the study we have just presented, a formal approach was used to validate a system that has already been implemented. Simulating the behavior of the system by means of a computer aided tool was what allowed us to nd problems in the implementation of the CRAB server. However, another great advantage of modeling a system with formal methods is the possibility to apply automatic analysis techniques to extract information about the system, like invariant analysis, and model checking.
In order to apply some of these techniques, the formal model must respect
specic prerequisites. For example, most algorithms for model checking a
concurrent system require a bounded state space. Nets-within-nets models which
satisfy this last requirement are hypernets [
The rst idea was to use such a class of nets to model the CRAB server, but because of the absence of modeling limitations and verication features in Renew, and because of the high complexity of the system, we preferred to use a slighty more powerful version of hypernets. To come back to the class of hypernets, having therefore the certainty that the state space is limited, the following xes are necessary:
Transitions which create or delete tokens must be deleted in some way. For example, transition crab -create of the CrabClient net cannot create an unbounded number of tasks anymore, but an input place which contains as many tokens as the maximum number of allowed tasks must be added. This is not a big problem. As a matter of fact the computers disks space is limited, and consequently so are the number of tasks which can be created by a user.
Hypernets use a value semantics, which means that a net cannot have two references to it. Nevertheless, in our model some transitions duplicate the references to a net. Duplication of references is somehow dangerous if the intention is to keep the state space bounded. Loosely speaking, the risk is of an uncontrolled grow of the references of a net without a corresponding deletion of these references. In our model the use of the value semantics can be achieved by deleting these duplications of references, and using simple tokens to communicate the intention to modify the referenced net.
Even though analysis of properties is not available with the current version of the model because of the issues just discussed, the more practicality of the reference semantics from a modeling point of view helped us nding several design defects in the implementation of the CRAB server. In the future we plan to restrict the model to a hypernet in order to be able to verify properties like invariants, or to do model checking 1. In our opinion, as a rst step it was 1 Restricting the model to hypernets is not the only way to have a limited state space, but a formal proof is available using hypernets thank’s to the 1-safe expansion Petri Nets & Concurrency { 281 important to use a powerful formalism to avoid getting lost in the details of the model, even though that meant sacricing the analysis capabilities. 6
In this paper, we discuss a large scale Grid application used to perform distributed data analysis in High Energy Physics experiments. Because of the complexity of the architecture, the software tool has been modeled using the netswithin-nets paradigm in order to validate the correctness of its behavior using simulation. In particular we considered the fundamental use case of the submission of user data analysis to the Grid. Every component of the CRABServer involved in this use case has been modeled in the hierarchy of the nets and compared to the behavior expected by its users.
From the simulation of the model a number of bugs and design defects emerged. This has led the developers to improve the overall quality of system implementation in the subsequent releases that the users now adopt. Two groups of bugs have been identied: bugs related to wrong coding of the expected behaviors and bugs where the specic adoption of nets-within-nets formalism has highlighted synchronization problems among the entities .
In addition, the approach followed to model the CRAB tool set has shown its generality in order to model most of the Grid applications in which an orchestration entity drives the nets representing both the nite state machines of the jobs running on the distributed infrastructure and the services exposing the resources themselves.
The class of nets used to model this system is a more powerful version of hypernets, using the reference semantics instead of the value semantics, and allowing creation/deletion of tokens. As discussed in Section 5, it is possible to restrict the model to a proper hypernet by sacricing its readability (some places and transitions must be added). Then, by means of hypernets and their expansion to 1-safe nets, it will be possible to use all the techniques dened for the class of 1-safe nets for analyzing the system.
A plugin of Renew that allows to draw and to analyze a hypernet is being developed. We plan to use this plugin to make automatic verication of properties of the system.