Proving the Completeness of the Composition of Two Dynamic Verification Techniques
There has been a significant amount of recent research in low-cost mechanisms for detecting errors in computer execution that are due to hardware faults. One exciting, low-cost approach to error detection is dynamic verification (sometimes also called online testing or runtime invariant checking). The idea is for the hardware to dynamically (i.e., at runtime) check whether certain necessary invariants are being maintained. In this paper, the authors prove that a combination of two previously developed dynamic verification schemes - the Argus scheme for processor cores and the Dynamic Verification of Memory Consistency (DVMC) scheme for the memory system - provides complete error detection for a multicore processor chip.