> 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.
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.
> 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.
> 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.
4 replies →
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.