QLOCK, a variant of Dijkstra’s binary semaphore, is a well known protocol of mutual exclusion, and many implementation and verifications in CafeOBJ are available. I have extended the current proofs of mutual exclusion to cover also fairness, i.e., any agent will eventually enter the queue and eventually go into critical section. Since this requires fairness of the execution, some meta constructs have to be reflected back into the specification.
My approach is to include an execution sequence in the modeling. The current code including documentation is her: qlock-freefair.cafe, which in turn needs the specification of the QLOCK protocol as given by Prof. Futatsugi for the lecture on Algebraic Formal Methods. The two files can be downloaded from there: qlock-sysProp.cafe and qlock-invPS.cafe.