Last active
May 15, 2019 05:53
-
-
Save lemmy/5cae084db688c06fbcb5faaa2f630dec to your computer and use it in GitHub Desktop.
BlockingQueue
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
--------------------------- 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