Analysis
A theoretical basis for the recovery model has been established.
Notion of safety defined.
Process dependency formalized.
A total ordering relation defined to describe the set of global state matrices formed during an execution.
Current global matrix proven to be the least upper bound of current set of matrices.
Recovery line defined and proven to be maximal and consistent.
Validation does not result in deadlock.