Hacker News Reader

Comment by aw1621107 | Hacker News Reader

> what if this bug is still there but the timing window is now one CPU instruction?

I think a model checker or something similar that can exhaustively cover a search space would suffice, though at that point I think the boundary between "test" and "formal verification" becomes somewhat fuzzy.

View on HN

> exhaustively cover a search space

This is the gotcha: in stateful environments you'll have state-space explosion so big you'll have to come up with some compromising measure of "equivalent". You're right that that would constitute a proof by exhaustion of correctness. Unfortunately in practice it's entirely impractical.

I was thinking that CDSChecker [0]-like tools like Rust's Loom [1] might be able to prune the write+checkpoint search space enough to make exhaustive checking feasible, though I'm far from knowledgeable enough about the implementation to say with any certainty how plausible my hunch is.

[0]: demsky.eecs.uci.edu/publications/c11modelcheck.pdf

[1]: https://docs.rs/loom/latest/loom/

So, a proof, not a test.

I mean, exhaustive tests are one way you can prove something.

You can't even exhaustively test every 64 bit integer value.

Just because you can't exhaustively test one thing doesn't mean you can't exhaustively test anything.

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

Reply on news.ycombinator.com