Comment by IX-103
14 days ago
Not being able to exhaustively test simple problem absolutely means you can't exhaustively test massively more complex problem. For a monotonically increasing function f, which I think we can agree a function mapping from the size of the input set to the runtime of an exhaustive execution of all elements in the set qualifies as, if |small| < |large| then f(small) < f(large). Therefore if f(small) is too big then f(large) is definitely too big.
> Not being able to exhaustively test simple problem absolutely means you can't exhaustively test massively more complex problem.
"Simple"/"complex" doesn't necessarily imply "small"/"large", respectively. Testing whether the Collatz conjecture holds is "simple", but its search space is (potentially) infinitely large. Testing correctness of concurrent data structures is (probably) a more "complex" problem, and yet it's still possible to perform exhaustive tests of their functionality [0].
In the end, the practicality of exhausting the 64-bit integer search space is irrelevant since it says nothing about the size of the write + checkpoint search space. I could just as easily say that it's easy to exhaust the 16-bit integer search space, but that doesn't mean exhaustively testing for this particular bug is easy.
[0]: http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf