The code is correct both practically and formally. All unordeeed reads are reading values written by the same thread. Even if the writes are atomic there is no violation of the no data races rule.