Recovery oriented programming: runtime monitoring of safety and liveness

摘要

We introduce the recovery-oriented programming paradigm. Programs that are designed according to the recovery-oriented programming paradigm include, as an integral part, the important safety and liveness properties that the program should respect and the recovery actions that should be executed upon a violation of these properties. We design a pre-compiler that compiles the properties and recovery actions into a code snippet for monitoring properties and enforcing recovery actions upon property violation. Assuming the restartability property of a given program and the existence of a self-stabilizing software platform, the compiled program is able to recover from safety and liveness violations. We provide a generic correctness proof scheme for recovery-oriented programs, proving that the code, as transformed by the pre-compiler, converges to a legal execution in a finite number of steps after experiencing an arbitrary failure.