3 ms·

no it can't. what if this bug is still there but the timing window is now one CPU instruction?

• aw1621107 3mo 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 3mo ago
    So, a proof, not a test.
    • aw1621107 3mo ago
      I mean, exhaustive tests are one way you can prove something.
      • inigyou 3mo ago
        You can't even exhaustively test every 64 bit integer value.
        • aw1621107 3mo ago
          Just because you can't exhaustively test one thing doesn't mean you can't exhaustively test anything.
          • IX-103 3mo 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.
            • aw1621107 3mo 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 3mo 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 3mo ago
      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/ https://docs.rs/loom/latest/loom/
• kccqzy 3mo ago
  Then it’s a different bug: they fixed a bug with a wider timing window and introduced a new bug with a narrower timing window.