17.5 Rules about Locks

By the pricking of my thumbs,
Something wicked this way comes.
Open, locks,
Whoever knocks!
—William Shakespeare, Macbeth, Act IV, scene i

Let T be a thread and L be a lock. There are certain constraints on the actions performed by T with respect to L:

• A lock action by T on L may occur only if, for every thread S other than T, the number of preceding unlock actions by S on L equals the number of preceding lock actions by S on L. (Less formally: only one thread at a time is permitted to lay claim to a lock, and moreover a thread may acquire the same lock multiple times and doesn't relinquish ownership of it until a matching number of unlock actions have been performed.)
• An unlock action by thread T on lock L may occur only if the number of preceding unlock actions by T on L is strictly less than the number of preceding lock actions by T on L. (Less formally: a thread is not permitted to unlock a lock it doesn't own.)

With respect to a lock, the lock and unlock actions performed by all the threads are performed in some total sequential order. This total order must be consistent with the total order on the actions of each thread.