Dynamic verification of end-to-end multiprocessor invariants
Daniel J. Sorin, M.D. Hill, David Alvra Wood · 2004
As implementations of shared memory multiprocessors become more complicated, hardware faults will increasingly cause errors that are difficult or impossible to detect with low-level, localized mechanisms. In this paper, we argue for dynamic verification (i.e., on-the-fly checking) of end-to-end, system-wide invariants in shared memory multiprocessors. We develop two invariant checkers based on distributed signature analysis. Our coherence-level checker dynamically verifies that every cache coherence upgrade has a corresponding downgrade elsewhere in the system. Our messagelevel checker verifies that all nodes in an SMP observe the same total order of broadcast requests. We use full-system simulation to show that the checkers detect the targeted errors while not significantly degrading system performance. 1