Spurious races due to non-atomic treatment of `__VERIFIER_atomic*`-prefixed functions

[sim642]

Although TSan excludes accesses from within these functions from racing, they aren't executed atomically (with the special atomic mutex held). This allows them to be interleaved, causing spurious races, e.g. with value-based mutex modeling.