This is true, and it falls into the "possible but not ergonomic" category for modeling systems like this in TLA+. Concurrent programs reading & writing to shared variables can be reordered at two levels: the compiler, and then the CPU. Specifying this in TLA+ is possible but difficult, and your conventional TLA+ specification will assume things happen in a linear order within each thread, and are interleaved arbitrarily between threads. In other words by default PlusCal works like there is both a barrier and memory fence between each action. Even with strong memory semantics like x86-TSO, specifying something like the action of the store buffer (where a core writes a value and can read the updated value but its write is not yet visible to other cores) requires actually writing your own tiny implementation of x86-TSO; there isn't one already defined as a library you can easily use.

I've been thinking lately about how to make this more ergonomic, as I've been getting into lock-free algorithms and would like to be able to specify them nicely in TLA+.