3 ms·
It can prove absence of specific bugs though.
by 0x457 2mo ago
It can prove absence of specific bugs though.
- inigyou 2mo agono it can't. what if this bug is still there but the timing window is now one CPU instruction?
- aw1621107 2mo ago> 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.
- inigyou 2mo agoSo, a proof, not a test.
- aw1621107 2mo agoI mean, exhaustive tests are one way you can prove something.
- inigyou 2mo agoYou can't even exhaustively test every 64 bit integer value.
- aw1621107 2mo agoJust because you can't exhaustively test one thing doesn't mean you can't exhaustively test anything.
- IX-103 2mo agoNot 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.
- aw1621107 2mo ago> 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 http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf
- ashton314 2mo ago> 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.
- aw1621107 2mo agoI 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/ https://docs.rs/loom/latest/loom/
- kccqzy 2mo agoThen it’s a different bug: they fixed a bug with a wider timing window and introduced a new bug with a narrower timing window.
- esjeon 2mo agoYou simply don't have enough testcases.