I think that's only half-useful, at best. If all your access to atomics happened to be mediated by, say, __atomic_cmpxchg, then modeling that as (say) atomic_compare_exchange_strong would give you confidence in the implementation. The problem is that pre-memory model code is also likely to check the current state of the atomic through a raw pointer load instead of anything like atomic_load (which generally has no counterpart in pre-memory model synchronization libraries). So, analyzing that code through the lens of C11 tells you little more than that it's undefined behavior.

Like most undefined behavior, it can work in practice. Probably. Most of the time. If you stick to using older compilers.