Operational RC11 ORC11
An operational version of RC11 (Operational RC11) developed for the RustBelt project. It underpins a program logic that was used to prove the soundness of several synchronisation primitives from the Rust standard library against the relaxed-memory semantics. Being equivalent to RC11, ORC11 is strictly stronger than the C++20 model Rust normatively ships (it forbids the out-of-thin-air, plain load-buffering and broken-release-sequence behaviours C++20 leaves open): it is the verification model RustBelt reasons against, a sound over-approximation of shipped Rust, not a model of its exact semantics.
Properties
Property vector survey-sourced — from Tables 1–2 of the Moiseenko et al. survey, except cells that cite a specific source.
- Compilation optimal mapping to
- yes x86
- no POWER
- no Armv7
- no Armv8
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- no Load→Store
- Elimination sound
- yes Store/Load
- yes Store/Store
- yes Load/Load
- no Load/Store
- Other local transformations
- no Speculative load intro.
- yes Roach motel
- yes Strengthening
- yes Trace preserving
- no Common subexpr. elim.
- Global transformations
- yes Register promotion
- yes Thread inlining
- Reasoning guarantees
- yes External DRF
- yes Coherence
- no No undefined behaviour
- yes In-order execution
- yes No out-of-thin-air
Ordering relationships
- Equivalent to
- Repaired C11 (RC11) — ORC11 is an operational version of RC11 developed for RustBelt to verify Rust standard-library synchronisation primitives against a program logic.
References
- Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer. RustBelt Meets Relaxed Memory. POPL 2020 (PACMPL vol. 4), 2019. doi:10.1145/3371102
- Evgenii Moiseenko, Anton Podkopaev, Dmitrii Koznov. A Survey of Programming Language Memory Models. Programming and Computer Software 47(6), pp. 439–456, 2021. doi:10.1134/S0361768821060050