{"id":49281134,"user":"inigyou","time":1786587841,"time_ago":"14 days ago","type":"comment","content":"

So, a proof, not a test.","comments":[{"id":49281297,"user":"aw1621107","time":1786589872,"time_ago":"14 days ago","type":"comment","content":"

I mean, exhaustive tests are one way you can prove something.","comments":[{"id":49283452,"user":"inigyou","time":1786612700,"time_ago":"14 days ago","type":"comment","content":"

You can't even exhaustively test every 64 bit integer value.","comments":[{"id":49284513,"user":"aw1621107","time":1786621238,"time_ago":"14 days ago","type":"comment","content":"

Just because you can't exhaustively test one thing doesn't mean you can't exhaustively test anything.","comments":[{"id":49286429,"user":"IX-103","time":1786630987,"time_ago":"14 days ago","type":"comment","content":"

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.","comments":[{"id":49290034,"user":"aw1621107","time":1786645508,"time_ago":"14 days ago","type":"comment","content":"

> 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","comments":[],"comments_count":0,"level":4,"url":"item?id=49290034"}],"comments_count":1,"level":3,"url":"item?id=49286429"}],"comments_count":2,"level":2,"url":"item?id=49284513"}],"comments_count":3,"level":1,"url":"item?id=49283452"}],"comments_count":4,"level":0,"url":"item?id=49281297"}],"comments_count":5,"url":"item?id=49281134"}

Comment by inigyou