3 ms·
> 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 comp
by 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/