Skip to content

Instantly share code, notes, and snippets.

@lemmy lemmy/BlockingQueue.tla
Last active May 15, 2019

Embed
What would you like to do?
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
You can’t perform that action at this time.