Cargando…
Analysis of DIRAC's behavior using model checking with process algebra
DIRAC is the grid solution developed to support LHCb production activities as well as user data analysis. It consists of distributed services and agents delivering the workload to the grid resources. Services maintain database back-ends to store dynamic state information of entities such as jobs, qu...
Autores principales: | , , , , , , , , , , |
---|---|
Lenguaje: | eng |
Publicado: |
2012
|
Materias: | |
Acceso en línea: | https://dx.doi.org/10.1088/1742-6596/396/5/052061 http://cds.cern.ch/record/1515980 |
_version_ | 1780928427478482944 |
---|---|
author | Remenska, Daniela Templon, Jeff Willemse, Tim Bal, Henri Verstoep, Kees Fokkink, Wan Charpentier, Philippe Diaz, Ricardo Graciani Lanciotti, Elisa Roiser, Stefan Ciba, Krzysztof |
author_facet | Remenska, Daniela Templon, Jeff Willemse, Tim Bal, Henri Verstoep, Kees Fokkink, Wan Charpentier, Philippe Diaz, Ricardo Graciani Lanciotti, Elisa Roiser, Stefan Ciba, Krzysztof |
author_sort | Remenska, Daniela |
collection | CERN |
description | DIRAC is the grid solution developed to support LHCb production activities as well as user data analysis. It consists of distributed services and agents delivering the workload to the grid resources. Services maintain database back-ends to store dynamic state information of entities such as jobs, queues, staging requests, etc. Agents use polling to check and possibly react to changes in the system state. Each agent's logic is relatively simple, the main complexity lies in their cooperation. Agents run concurrently, and collaborate using the databases as shared memory. The databases can be accessed directly by the agents if running locally or through a DIRAC service interface if necessary. This shared-memory model causes entities to occasionally get into inconsistent states. Tracing and fixing such problems becomes formidable due to the inherent parallelism present. We propose more rigorous methods to cope with this. Model checking is one such technique for analysis of an abstract model of a system. Unlike conventional testing, it allows full control over the parallel processes execution, and supports exhaustive state-space exploration. We used the mCRL2 language and toolset to model the behavior of two related DIRAC subsystems: the workload and storage management system. Based on process algebra, mCRL2 allows defining custom data types as well as functions over these. This makes it suitable for modeling the data manipulations made by DIRAC's agents. By visualizing the state space and replaying scenarios with the toolkit's simulator, we have detected race-conditions and deadlocks in these systems, which, in several cases, were confirmed to occur in the reality. Several properties of interest were formulated and verified with the tool. Our future direction is automating the translation from DIRAC to a formal model. |
id | cern-1515980 |
institution | Organización Europea para la Investigación Nuclear |
language | eng |
publishDate | 2012 |
record_format | invenio |
spelling | cern-15159802022-08-17T13:24:46Zdoi:10.1088/1742-6596/396/5/052061http://cds.cern.ch/record/1515980engRemenska, DanielaTemplon, JeffWillemse, TimBal, HenriVerstoep, KeesFokkink, WanCharpentier, PhilippeDiaz, Ricardo GracianiLanciotti, ElisaRoiser, StefanCiba, KrzysztofAnalysis of DIRAC's behavior using model checking with process algebraComputing and ComputersDIRAC is the grid solution developed to support LHCb production activities as well as user data analysis. It consists of distributed services and agents delivering the workload to the grid resources. Services maintain database back-ends to store dynamic state information of entities such as jobs, queues, staging requests, etc. Agents use polling to check and possibly react to changes in the system state. Each agent's logic is relatively simple, the main complexity lies in their cooperation. Agents run concurrently, and collaborate using the databases as shared memory. The databases can be accessed directly by the agents if running locally or through a DIRAC service interface if necessary. This shared-memory model causes entities to occasionally get into inconsistent states. Tracing and fixing such problems becomes formidable due to the inherent parallelism present. We propose more rigorous methods to cope with this. Model checking is one such technique for analysis of an abstract model of a system. Unlike conventional testing, it allows full control over the parallel processes execution, and supports exhaustive state-space exploration. We used the mCRL2 language and toolset to model the behavior of two related DIRAC subsystems: the workload and storage management system. Based on process algebra, mCRL2 allows defining custom data types as well as functions over these. This makes it suitable for modeling the data manipulations made by DIRAC's agents. By visualizing the state space and replaying scenarios with the toolkit's simulator, we have detected race-conditions and deadlocks in these systems, which, in several cases, were confirmed to occur in the reality. Several properties of interest were formulated and verified with the tool. Our future direction is automating the translation from DIRAC to a formal model.oai:cds.cern.ch:15159802012 |
spellingShingle | Computing and Computers Remenska, Daniela Templon, Jeff Willemse, Tim Bal, Henri Verstoep, Kees Fokkink, Wan Charpentier, Philippe Diaz, Ricardo Graciani Lanciotti, Elisa Roiser, Stefan Ciba, Krzysztof Analysis of DIRAC's behavior using model checking with process algebra |
title | Analysis of DIRAC's behavior using model checking with process algebra |
title_full | Analysis of DIRAC's behavior using model checking with process algebra |
title_fullStr | Analysis of DIRAC's behavior using model checking with process algebra |
title_full_unstemmed | Analysis of DIRAC's behavior using model checking with process algebra |
title_short | Analysis of DIRAC's behavior using model checking with process algebra |
title_sort | analysis of dirac's behavior using model checking with process algebra |
topic | Computing and Computers |
url | https://dx.doi.org/10.1088/1742-6596/396/5/052061 http://cds.cern.ch/record/1515980 |
work_keys_str_mv | AT remenskadaniela analysisofdiracsbehaviorusingmodelcheckingwithprocessalgebra AT templonjeff analysisofdiracsbehaviorusingmodelcheckingwithprocessalgebra AT willemsetim analysisofdiracsbehaviorusingmodelcheckingwithprocessalgebra AT balhenri analysisofdiracsbehaviorusingmodelcheckingwithprocessalgebra AT verstoepkees analysisofdiracsbehaviorusingmodelcheckingwithprocessalgebra AT fokkinkwan analysisofdiracsbehaviorusingmodelcheckingwithprocessalgebra AT charpentierphilippe analysisofdiracsbehaviorusingmodelcheckingwithprocessalgebra AT diazricardograciani analysisofdiracsbehaviorusingmodelcheckingwithprocessalgebra AT lanciottielisa analysisofdiracsbehaviorusingmodelcheckingwithprocessalgebra AT roiserstefan analysisofdiracsbehaviorusingmodelcheckingwithprocessalgebra AT cibakrzysztof analysisofdiracsbehaviorusingmodelcheckingwithprocessalgebra |