Comment by ashton314
14 days 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.
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/