BlockingQueue

BlockingQueue.cfg

@@ -0,0 +1,23 @@
+SPECIFICATION BQSpec
+
+INVARIANT 
+    TypeOK
+
+PROPERTIES 
+    DeadlockFree
+    \* Foo
+    StarvationFreedom
+
+CONSTANT
+    bufCap = 4
+
+    p1 = p1
+    p2 = p2
+    p3 = p3
+    p4 = p4
+    P = {p1,p2,p3,p4}
+
+    c1 = c1
+    c2 = c2
+    c3 = c3
+    C = {c1,c2,c3}

BlockingQueue.tla

@@ -0,0 +1,80 @@
+----- MODULE BlockingQueue -----
+EXTENDS Naturals, FiniteSets    
+
+CONSTANT bufCap, P, C
+
+ASSUME /\ bufCap \in Nat
+       /\ IsFiniteSet(P)
+       /\ P # {}
+       /\ IsFiniteSet(C)
+       /\ C # {}
+
+VARIABLE buf, waitSet
+vars == <<buf, waitSet>>
+
+TypeOK ==
+    /\ buf \in 0..bufCap
+    /\ waitSet \in SUBSET (P \union C)
+
+Init ==
+    /\ buf = 0
+    /\ waitSet = {}
+
+Notify ==
+    IF waitSet = {} THEN UNCHANGED waitSet
+    ELSE \E t \in waitSet: waitSet' = waitSet \ {t}
+
+NotifyAll ==
+    waitSet' = {}
+
+NotifyOther(T) ==
+    IF waitSet \cap T = {} THEN UNCHANGED waitSet
+    ELSE \E t \in waitSet \cap T : waitSet' = waitSet \ {t}
+
+Wait(self) ==
+    waitSet' = waitSet \union {self}
+
+Put(self) ==
+    \/ /\ bufCap > buf
+       /\ buf' = buf + 1
+       /\ Notify
+    \/ /\ bufCap = buf
+       /\ Wait(self)
+       /\ UNCHANGED buf
+
+Get(self) ==
+    \/ /\ buf > 0
+       /\ buf' = buf - 1
+       /\ Notify
+    \/ /\ buf = 0
+       /\ Wait(self)
+       /\ UNCHANGED buf
+
+Next ==
+    \E t \in (P \union C) \ waitSet:
+        \/ /\ t \in P
+           /\ Put(t)
+        \/ /\ t \in C
+           /\ Get(t)
+
+BQSpec ==
+    Init /\ [][Next]_vars /\ WF_vars(Next)
+
+DeadlockFree ==
+    [](waitSet # P \union C)
+
+Foo ==
+    <>(buf = bufCap)
+
+\* BQ => DeadlockFree
+\* BQS => DeadlockFree
+\* BQS => BQ
+
+\* <>[]P
+\* []<>P
+
+StarvationFreedom ==
+    /\ \A p \in P: []<> <<Put(p)>>_<<buf,waitSet>>
+    /\ \A c \in C: []<> <<Get(c)>>_<<buf,waitSet>>
+
+====

BlockingQueueSplit.cfg

@@ -0,0 +1,22 @@
+INIT Init
+NEXT Next
+
+INVARIANT 
+    TypeOK
+
+PROPERTIES 
+    BQSpec
+
+CONSTANT
+    bufCap = 1
+
+    p1 = p1
+    p2 = p2
+    p3 = p3
+    p4 = p4
+    P = {p1}
+
+    c1 = c1
+    c2 = c2
+    c3 = c3
+    C = {c1,c2}

BlockingQueueSplit.tla

@@ -0,0 +1,70 @@
+----- MODULE BlockingQueueSplit ------
+EXTENDS Naturals, FiniteSets    
+
+CONSTANT bufCap, P, C
+
+ASSUME /\ bufCap \in Nat
+       /\ IsFiniteSet(P)
+       /\ P # {}
+       /\ IsFiniteSet(C)
+       /\ C # {}
+
+VARIABLE buf, waitSetC, waitSetP
+vars ==<<buf, waitSetC, waitSetP>>
+
+TypeOK ==
+    /\ buf \in 0..bufCap
+    /\ waitSetC \in SUBSET (C)
+    /\ waitSetP \in SUBSET (P)
+
+Init ==
+    /\ buf = 0
+    /\ waitSetC = {}
+    /\ waitSetP = {}
+
+Notify(ws) ==
+    IF ws = {} THEN UNCHANGED ws
+    ELSE \E t \in ws: ws' = ws \ {t}
+
+Wait(ws, self) ==
+    ws' = ws \union {self}
+
+Put(self) ==
+    \/ /\ bufCap > buf
+       /\ buf' = buf + 1
+       /\ Notify(waitSetC)
+       /\ UNCHANGED waitSetP
+    \/ /\ bufCap = buf
+       /\ Wait(waitSetP, self)
+       /\ UNCHANGED <<buf, waitSetC>>
+
+Get(self) ==
+    \/ /\ buf > 0
+       /\ buf' = buf - 1
+       /\ Notify(waitSetP)
+       /\ UNCHANGED waitSetC
+    \/ /\ buf = 0
+       /\ Wait(waitSetC, self)
+       /\ UNCHANGED <<buf, waitSetP>>
+
+Next ==
+    \E t \in (P \union C) \ (waitSetC \union waitSetP):
+        \/ /\ t \in P
+           /\ Put(t)
+        \/ /\ t \in C
+           /\ Get(t)
+
+BQSSpec ==
+    Init /\ [][Next]_vars
+
+\* BQS => BQ
+
+BQ ==
+    INSTANCE BlockingQueue WITH waitSet <- waitSetP \union waitSetC
+
+BQSpec ==
+    BQ!BQSpec
+
+THEOREM Implements == BQSSpec => BQSpec
+THEOREM Types == BQSSpec => TypeOK
+=====