An efficient validation approach for quasi-synchronous checkpointing oriented to distributed diagnosability

The autonomic computing paradigm is oriented towards enabling complex distributed systems to manage themselves, even in faulty situations. The diagnosability analysis is a priori a study through which a system can be self-aware about its current state. It is from the determination of a consistent state that a system can take some action to repair or reconfigure itself. Nevertheless, in a distributed system it is hard to determine consistent states since we cannot observe simultaneously all the local variables of different processes. In this context, the challenge is to efficiently monitor the system execution over time to capture trace information in order to determine if the system accomplishes both functional and non-functional requirements. Quasi-synchronous checkpointing is a technique that collects information from which a system can establish consistent snapshots. Based on this technique, several checkpointing algorithms have been developed. According to the checkpoint properties detected and ensured, they are classified into: Strictly Z-Path Free (SZPF), Z-Path Free (ZPF) and Z-Cycle Free (ZCF). Generally, the method adopted for the performance evaluation of checkpointing algorithms involves simulation. However, few works have been designed to validate their correctness. In this paper, we propose an efficient validation approach based on a graph transformation oriented towards the automatic detection of the previously mentioned properties. To achieve this, we took the vector clocks resulting from an algorithm execution, and we modeled them into the happened-before graph and the immediate dependency graph (which is the minimal causal graph). Then, we designed a set of transformation rules to verify if in these graphs, the algorithm is exempt from non-desirable patterns, such as Z-paths or Z-cycles, according to the case.