The domino effect as a deadlock

The possibility of effects like an unpredictable growth of resource and com putation time losses and of expenditures on recovery (e.g. the domino effec t) makes backward recovery schemes unpracticable for systems with high faul t-tolerance requirements, although they have a number of advantages. The ma in purpose of this paper is to propose a formal model of the execution of c oncurrent programs, in which the domino effect can happen, and of the way t his effect can be detected statically by analysing the programs. In particu lar, this can be done by reducing the domino effect problem to that of dete cting a deadlock condition. This would allow the existing techniques for an alysing the correctness of concurrent systems and detecting deadlocks stati cally to be used to analyse the properties of recovering systems and static ally obtain additional information on the behaviour of concurrent systems i n the event of a fault and rollback. By performing a static analysis of all system paths (which relies on looking through the entire reachability tree of process joint behaviours), several behavioural system properties concer ning recovery can be checked prior to system use. Detecting bottle-necks at the system design stage will help to avoid unpredictable resource expendit ures, and their elimination will help to ensure certain properties of syste m behaviour when recovering from faults.