This paper explores the idea that redundant operations, like type errors, commonly flag correctness errors. We experimentally test this idea by writing and applying four redundancy checkers to the Linux operating system, finding many errors. We then use these errors to demonstrate that redundancies, even when harmless, strongly correlate with the presence of traditional hard errors (e.g., null pointer dereferences, unreleased locks). Finally we show that how flagging redundant operations gives a way to make specifications "fail stop" by detecting dangerous omissions. Keywords Extensible compilation, error detection. General Terms Reliability, Security, Verification. Categories and Subject Descriptors Software [Software Engineering]: Software/Program Verification
Yichen Xie, Dawson R. Engler