This is a little optimistic: being able to tractibly reason about atomicity in weak memory models like C11 is still at the cutting edge of CS research. It is really hard to prove nontrivial data structures are correct.