This is simply not true. Rust borrow checker has no notion of memory models: i.e. sequential consistency, acquire, release or relaxed semantics.
The Tokio team needs an additional model checker to ensure no data race in Tokio:
- https://github.com/tokio-rs/loom
If you want to ensure no data races you need formal verification not a borrow checker, I've compiled my research and a RFC for Nim formal verification here:
- https://github.com/mratsim/weave/issues/18
- https://github.com/nim-lang/RFCs/issues/222