Using model checking to analyze the system behavior of the LHC production grid |
| |
Authors: | Daniela Remenska Tim A.C. Willemse Kees Verstoep Jeff Templon Henri Bal |
| |
Affiliation: | 1. Department of Computer Science, VU University Amsterdam, The Netherlands;2. Department of Computer Science, TU Eindhoven, The Netherlands;3. NIKHEF National Institute for High-Energy Physics, Amsterdam, The Netherlands |
| |
Abstract: | DIRAC (Distributed Infrastructure with Remote Agent Control) is the grid solution designed to support production activities as well as user data analysis for the Large Hadron Collider “beauty” experiment. It consists of cooperating distributed services and a plethora of light-weight agents delivering the workload to the grid resources. Services accept requests from agents and running jobs, while agents actively fulfill specific goals. Services maintain database back-ends to store dynamic state information of entities such as jobs, queues, or requests for data transfer. Agents continuously check for changes in the service states and react to these accordingly. The logic of each agent is rather simple; the main source of complexity lies in their cooperation. These agents run concurrently and communicate using the services’ databases as a shared memory for synchronizing the state transitions. Despite the effort invested in making DIRAC reliable, entities occasionally get into inconsistent states. Tracing and fixing such behaviors is difficult, given the inherent parallelism among the distributed components and the size of the implementation.In this paper we present an analysis of DIRAC with mCRL2, process algebra with data. We have reverse engineered two critical and related DIRAC subsystems, and subsequently modeled their behavior with the mCRL2 toolset. This enabled us to easily locate race conditions and livelocks which were confirmed to occur in the real system. We further formalized and verified several behavioral properties of the two modeled subsystems. |
| |
Keywords: | Model checking Process algebra Grid LHC Distributed system Workflow |
本文献已被 ScienceDirect 等数据库收录! |
|