Let's keep a list of all the cases where GenMC mode is not able to execute correct Rust code properly

• Temporal mixing of atomic and non-atomic accesses: GenMC doesn't know about the non-atomic accesses that occurred, so an atomic load can return invalid results. In Rust, the "initializing" write is usually always non-atomic (either a call to Atomic*::new, or the initial value of a static), so currently manual calls to store are required to work around this.
• Mixed-size accesses: Rust allows racing mixed-size accesses as long as all accesses are reads; GenMC does not support this, which can lead to loads returning invalid results. In fact, GenMC does not support any kind of mixed-size accesses (but non-atomic accesses are still handled by Miri so we only notice this for atomic accesses): even in sequential code, if the initializing non-atomic write used a different size than a later atomic read, we get an error ("mixed-size" if the atomic read uses the same address but different size than the non-atomic write; "uninitialized memory" if the atomic read is offset into the middle of the non-atomic write).
• Optimized local variables being moved into memory: when a local variable is moved from its efficient representation as an Immediate to its in-memory representation, GenMC thinks the write happens then and there, whereas really the write happened earlier. This can leas to GenMC reporting a data race when there is none.
• Incorrect wrapping behavior of fetch_add/sub: GenMC internally always uses 64bit arithmetic, so its internal value can diverge from what he program sees. This is relevant when a fetch_add is followed by a fetch_max, as the latter can then pick the wrong result.
• The per-thread memory allocator will "overflow" when the 4GB limit is reached, leading to duplicate addresses being handed out. There are also some integer overflows with sufficiently large sizes or alignments.
• GenMC's tracking of uninitialized memory does not match the Rust model.
• Anything that mutates global state not tracked by GenMC is a potential problem since GenMC expects that threads do not influence each other. This includes any use of the RNG, the file descriptor table, and more.
• Needs further exploration: GenMC implement pthread lock semantics, but Rust locks are movable, so this might lead to incorrect error reports.

Cc @Patrick-6 -- please let me know if I missed anything