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(sq(S:Sys))= I:X$Pid if pc(S:Sys,I:X$Pid)= cs [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 pc(S:Sys,I:X$Pid)= cs /\ pc(S:Sys,J:X$Pid)= cs ;

See qgoal.maude for the full proof.