This is a model of a CLH lock, based on the paper by Travis Craig titled Building FIFO and priority-queueing spin locks from atomic swap,” Technical Report TR 93-02-02, Department of Computer Science, University of Washington, February, 1993.
For details, see my blog post Modeling a CLH lock in TLA+.