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 f

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/