Mutual Exclusion Protocol (QLOCK)

Assume that many agents (or processes) are competting for a common resource, but that at any given moment of time only one agent can use the resource. That is, the agents exclude or prevent each other from accessing the resource. A protocol that can gurantee this kind of mutual-exclusion property is called a mutual exclusion protocol (slides).

Specification

See qlock.maude for the full specification.

Verification

If a process/agent is in the critical section, then it is at the top of waiting queue.

QLOCK |- ceq top(Q:Sequence)= I:X$Pid if < Q:Sequence,< I:X$Pid,cs > A:Set > := S:Reach [nonexec] ;

See qinv.maude for the full proof.

Only one agent can be in the critical section at a given moment.

GOAL |- ceq I:X$Pid = J:X$Pid if < Q:Sequence,< I:X$Pid,cs > < J:X$Pid,cs > A:Set > : Reach ;

See qgoal.maude for the full proof.