Loom model checking

[loyd]

I understand this requires a vast amount of work. However, at least an issue should exist.

Except for using loom's primitives for testing, I think it should use them under --cfg scc_loom (in the same way as crossbeam_loom exists) to support testing in implementation of structures based on scc-ebr implementation.

[loyd]

@wvwwvwwv, what does "Formally verified EBR" in README mean? Is it about https://github.com/wvwwvwwv/scalable-concurrent-containers/blob/main/src/tests/model.rs?

[wvwwvwwv]

I also know that the loom tests in the crate is not ideal. At my previous workplace, I used a generalised atomic interface to avoid any use of compile-time flags, so I may try this approach here as well.

Please don't pay much attention to Formally verified EBR part :-) It just means that I developed ebr along with those loom tests; doesn't mean that I used Coq or the likes to formally prove the algorithm. Note that the use of every memory barrier/fence was justified internally in my previous company, though, I cannot disclose any part of it.

[shamilsan]

Let me try to implement some loom-based tests as a sponsored work backed by @loyd.

[loyd]

I close this issue in favor of https://github.com/wvwwvwwv/scalable-delayed-dealloc/issues/1 due to https://github.com/wvwwvwwv/scalable-concurrent-containers/issues/131