Test & Set (TAS)

Test & Set (TAS) is a mutual-exclusion protocol where several concurrent processes make use of a shared lock to ensure that, at any moment of time, at most one process is in a critical section. In a nutshell, the protocol works as follows:

• Initially, the lock is open, and all processes are in a so-called remainder section.
• At each step, any process may attempt to acquire the lock. If the lock is open, then the process obtains it (in the same single, atomic operation) and enters the critical section; otherwise, the process continues its execution in the remainder section.
• Any process can leave the critical section at any time, thus opening the lock.

A snapshot of the protocol can be found here.

Specification

See tas.maude for the full specification.

Verification

For TAS, we are interested in verifying the following strong mutual-exclusion property: at every moment of time, at most one process is in a critical section, in which case the lock is closed.

We formalize this property as a conjunction of two goals (defined in this case as contradictions; cf. the OTS/CafeOBJ method) that are proved simultaneously.

The lock is closed whenever a process is in a critical section

ceq true = false if < open, (cs LS:LSet) > := R:Reach ;

At most one process is in a critical section

ceq true = false if < S:Status, (cs cs LS:LSet) > := R:Reach ;

See me.maude for the full proof.