A domino-effect free recovery algorithm: formal specification

Recovery techniques may be distinguished on the basis of the time when the recovery lines are built: at the time of recording the recovery point, at the time of rollback; Consequently we distinguish "planned" and "unplanned" policies for determining recovery lines. With an unplanned policy a "domino effect" can occur, with increase of rollback activity and unknown amount of process elaboration to be undone. The planned policy is usually intended as being static, in the sense that the recovery lines are a priori established at design time. In this paper an algorithm for "dynamic" planning or recovery line is formally specified. We shall define a computational model for a distributed system of communicating processes using asynchronous message passing and shall describe the recovery algorithms by means of axioms.