BlockingQueue

BlockingQueue.tla

--------------------------- MODULE BlockingQueueBlog ---------------------------
EXTENDS Naturals, Sequences, FiniteSets, TLC

C == {"a", "b"}   \* Two consumers and producers...
P == {"c", "d"}   \* ...which are usually better model as sets of model values.
K == 1            \* Fix queue size to 1 element

\* We assume the following properties even though the spec doesn't use CONSTANTS.
ASSUME /\ IsFiniteSet(C) /\ IsFiniteSet(P) \* Finite sets
       /\ C \intersect P = {}              \* A producer is no consumer and vice versa
ASSUME K \in (Nat \ {0})                   \* K is a natural number without zero

------------------------------------------------------------------

\* Nondeterministically notify (wake) a process from the given waitset.
Notify(w) == IF w # {}
             THEN \E i \in w: w' = w \ {i}
             ELSE UNCHANGED << w >>

------------------------------------------------------------------

VARIABLES store, \* The (internal) storage for the queue
          waitP, \* A waitset for producers
          waitC  \* A waitset for consumers
vars == << store, waitP, waitC >>

\* A type correctness invariant asserting that...
TypeOK == /\ waitP \subseteq P \* only producers are in waitP
          /\ waitC \subseteq C \* only consumers are in waitC
          /\ DOMAIN store \subseteq 0..K \* store is a sequence for which the 
                                         \* elements of the codomain are undefined.

(***************************************************************************)
(* Initially consumers and processes are alive and the queue is empty.     *)
(***************************************************************************)
Init == /\ store = <<>>
        /\ waitP = {}
        /\ waitC = {}

(***************************************************************************)
(* A producer either waits if the queue is full or appends an element.     *)
(***************************************************************************)
p1(self) == /\ Len(store) = K
            /\ waitP' = (waitP \cup {self})
            /\ UNCHANGED << store, waitC >>

p2(self) == /\ Len(store) # K
            /\ Notify(waitC)
            /\ store' = Append(store, self)
            /\ UNCHANGED << waitP >>

(***************************************************************************)
(* A consumer either waits if the queue is empty (c1) or picks one element *)
(* (c2). c2 is the critical section from the perspective of the consumer.  *)
(***************************************************************************)
c1(self) == /\ Len(store) = 0
            /\ waitC' = (waitC \cup {self})
            /\ UNCHANGED << store, waitP >>

c2(self) == /\ Len(store) # 0
            /\ Notify(waitP)
            /\ store' = Tail(store)
            /\ UNCHANGED << waitC >>
            
(***************************************************************************)
(* Let the scheduler non-deterministically schedule consumer and           *)
(* producers processes.                                                    *)
(*                                                                         *)
(* Correct Next to not schedule waiting processes. Thanks to Hillel for    *)
(* making me aware of this issue.                                          *)
(***************************************************************************)
Next == \/ (\E self \in (P \ waitP): p1(self) \/ p2(self))
        \/ (\E self \in (C \ waitC): c1(self) \/ c2(self))
        

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
THEOREM Spec => []TypeOK

------------------------------------------------------------------

\* Not all consumers and producers wait at once.
NoDeadLock == (waitP \cup waitC) # (C \cup P)
THEOREM Spec => []NoDeadLock

\* All consumers eventually dequeue elements.
NoCStarvation == \A c \in C: []<>(<<c2(c)>>_<<store>>)

\* All producers eventually enqueue elements.
NoPStarvation == \A p \in P: []<>(<<p2(p)>>_<<store>>)
=============================================================================