[OJFord]

Well it's not a general purpose programming language defining the actual lock this way, it's checking a locking algorithm; so the atomic in the specification of the algorithm is just saying given that these steps do occur atomically, how will it behave.

The algorithm we're checking is using Redis, and the atomic read/write in the example is a behaviour Redis gives you.