-- -- Mutual Exclusion Algorithm using Queue -- -- We write a program called QLOCK that allows at most one process to -- execute the critical section at any given time. -- QLOCK uses a queue where processes wait for entering the critical -- section. -- all operations of the queue are supposed to be atomic. -- -- - put(queue,i) atomically puts process i into the queue at the end. -- - get(queue) atomically deletes the top process of the queue if any. -- - top(queue) atomically returns the top process of the queue if any. -- -- The queue is initially empty. -- -- QLOCK is as follows: -- -- l1: put(queue,i); -- l2: if (i != top(queue)) goto l2; -- Critical Section -- cs: get(queue); -- -- The formal model of the program: -- - Three transition rules are used. -- * 'want_i' corresponds to 'put(queue,i)'. -- * 'try_i' corresponds to 'if (i != top(queue)) goto l2'. -- * 'exit_i' corresponds to 'get(queue)'. -- - Two observable values are used. -- * 'queue' denotes the queue. -- * 'pc_i' indicates where process i is at. -- -- In the formal model, we use three kinds of data types: lables, -- process IDs and queues. -- If we prove QLOCK mutually exclusive, we need lemmas on queues. -- Here we take a careful look at module QUEUE where queues are -- defined. -- mod! LABEL { [Label] ops l1 l2 cs : -> Label op _=_ : Label Label -> Bool {comm} var L : Label eq (L = L) = true . eq (l1 = l2) = false . eq (l1 = cs) = false . eq (l2 = cs) = false . } mod* PID { [Pid] op _=_ : Pid Pid -> Bool {comm} var I : Pid eq (I = I) = true . } -- -- Instead of queues of a specific data type, queues of an any data -- type is defined. -- Therefore, we use a parameterized module to define such generic -- queues. -- First module EQTRIV that is used as a formal parameter of the -- parameterized module. -- EQTRIV declares that an actual parameter with which the -- parametrized module is instantiated should have one visible sort -- and operator _=_. -- mod* EQTRIV { [Elt] op _=_ : Elt Elt -> Bool {comm} } -- -- Then, the parameterized module for generic queues can be declared. -- mod! QUEUE (D :: EQTRIV) { [Queue] -- constructors op empty : -> Queue op __ : Elt.D Queue -> Queue -- operators op put : Queue Elt.D -> Queue op get : Queue -> Queue op top : Queue -> Elt.D op empty? : Queue -> Bool op _\in_ : Elt.D Queue -> Bool -- CafeOBJ variables var Q : Queue vars X Y : Elt.D -- equations eq put(empty,X) = X empty . eq put((Y Q),X) = Y put(Q,X) . eq get(empty) = empty . eq get((X Q)) = Q . eq top((X Q)) = X . eq empty?(empty) = true . eq empty?((X Q)) = false . eq X \in empty = false . eq X \in (X Q) = true . ceq X \in (Y Q) = X \in Q if not(X = Y) . -- -- The following equations are needed for the verification that QLOCK -- is mutually exclusive. -- The equations can be deduced from the above equations. -- You can find the proofs in queue.mod. -- -- used in proof2.mod ceq (top(put(Q,Y)) = X) = true if not empty?(Q) and top(Q) = X . -- used in proof3.mod eq empty?(put(Q,X)) = false . ceq X \in Q = false if empty?(Q) . -- used in proof4.mod eq X \in put(Q,X) = true . ceq X \in put(Q,Y) = true if X \in Q . } mod* QLOCK { pr(LABEL + PID) pr(QUEUE(PID)) *[Sys]* -- any initial state op init : -> Sys -- observations bop pc : Sys Pid -> Label bop queue : Sys -> Queue -- actions bop want : Sys Pid -> Sys bop try : Sys Pid -> Sys bop exit : Sys Pid -> Sys -- CafeOBJ variables var S : Sys vars I J : Pid -- for any initial state eq pc(init,I) = l1 . eq queue(init) = empty . -- for want op c-want : Sys Pid -> Bool {strat: (0 1 2)} eq c-want(S,I) = (pc(S,I) = l1) . -- ceq pc(want(S,I),J) = (if I = J then l2 else pc(S,J) fi) if c-want(S,I) . ceq queue(want(S,I)) = put(queue(S),I) if c-want(S,I) . ceq want(S,I) = S if not c-want(S,I) . -- for try op c-try : Sys Pid -> Bool {strat: (0 1 2)} eq c-try(S,I) = (pc(S,I) = l2 and top(queue(S)) = I) . -- ceq pc(try(S,I),J) = (if I = J then cs else pc(S,J) fi) if c-try(S,I) . eq queue(try(S,I)) = queue(S) . ceq try(S,I) = S if not c-try(S,I) . -- for exit op c-exit : Sys Pid -> Bool {strat: (0 1 2)} eq c-exit(S,I) = (pc(S,I) = cs) . -- ceq pc(exit(S,I),J) = (if I = J then l1 else pc(S,J) fi) if c-exit(S,I) . ceq queue(exit(S,I)) = get(queue(S)) if c-exit(S,I) . ceq exit(S,I) = S if not c-exit(S,I) . }