BlockingQueue
--------------------------- 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>>) | |
============================================================================= |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment