diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 5e44c46..92f2d0c 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -9,24 +9,16 @@ jobs: steps: - uses: actions/checkout@v1 - # Do not download and install TLAPS over and over again. - - uses: actions/cache@v1 - id: cache - with: - path: tlaps/ - key: tlaps1.4.5 + - name: Get CommunityModules + run: wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules.jar - name: Extract CommunityModules for TLAPS run: unzip CommunityModules.jar -d CommunityModules/ - name: Get TLAPS - if: steps.cache.outputs.cache-hit != 'true' # see actions/cache above - run: wget https://github.com/tlaplus/tlapm/releases/download/v1.4.5/tlaps-1.4.5-x86_64-linux-gnu-inst.bin + run: wget https://github.com/tlaplus/tlapm/releases/download/1.6.0-pre/tlapm-1.6.0-pre-x86_64-linux-gnu.tar.gz - name: Install TLAPS - if: steps.cache.outputs.cache-hit != 'true' # see actions/cache above - run: | - chmod +x tlaps-1.4.5-x86_64-linux-gnu-inst.bin - ./tlaps-1.4.5-x86_64-linux-gnu-inst.bin -d tlaps + run: tar -xzf tlapm-1.6.0-pre-x86_64-linux-gnu.tar.gz - name: Run TLAPS - run: tlaps/bin/tlapm --cleanfp -I tlaps/ -I CommunityModules/ BlockingQueue.tla BlockingQueueSplit.tla BlockingQueueFair.tla + run: tlapm/bin/tlapm --cleanfp -I CommunityModules/ BlockingQueue.tla BlockingQueueSplit.tla BlockingQueueFair.tla BlockingQueuePoisonApple_proofs.tla - name: Get (nightly) TLC run: wget https://nightly.tlapl.us/dist/tla2tools.jar - name: Run TLC diff --git a/BlockingQueueFair.tla b/BlockingQueueFair.tla index 4c6fc6e..e137251 100644 --- a/BlockingQueueFair.tla +++ b/BlockingQueueFair.tla @@ -1,5 +1,5 @@ ------------------------- MODULE BlockingQueueFair ------------------------- -EXTENDS Naturals, Sequences, FiniteSets, Functions, SequencesExt, SequencesExtTheorems +EXTENDS Naturals, Sequences, FiniteSets, Functions, SequencesExt, SequenceTheorems CONSTANTS Producers, (* the (nonempty) set of producers *) Consumers, (* the (nonempty) set of consumers *) @@ -85,7 +85,8 @@ BQSStarvation == BQS!A!Starvation THEOREM FairSpec => BQSStarvation ----------------------------------------------------------------------------- -TypeInv == /\ Len(buffer) \in 0..BufCapacity +TypeInv == /\ buffer \in Seq(Producers) + /\ Len(buffer) \in 0..BufCapacity \* Producers /\ waitSeqP \in Seq(Producers) /\ IsInjective(waitSeqP) \* no duplicates (thread is either asleep or not)! @@ -112,13 +113,13 @@ THEOREM ITypeInv == Spec => []TypeInv /\ buffer' = Append(buffer, p) /\ NotifyOther(waitSeqC) /\ UNCHANGED waitSeqP - BY <3>1, <2>1, TailTransitivityIsInjective + BY <3>1, <2>1, TailInjectiveSeq DEF NotifyOther, IsInjective <3>2. CASE /\ Len(buffer) = BufCapacity /\ Wait(waitSeqP, p) /\ UNCHANGED waitSeqC \* Put below so TLAPS knows about t \notin Range(waitSeqP) - BY <3>2, <2>1, AppendTransitivityIsInjective + BY <3>2, <2>1, AppendInjectiveSeq DEF Wait, IsInjective, Put <3>3. QED BY <2>1, <3>1, <3>2 DEF Put @@ -129,13 +130,13 @@ THEOREM ITypeInv == Spec => []TypeInv /\ buffer' = Tail(buffer) /\ NotifyOther(waitSeqP) /\ UNCHANGED waitSeqC - BY <3>1, <2>2, TailTransitivityIsInjective + BY <3>1, <2>2, TailInjectiveSeq, HeadTailProperties DEF NotifyOther, IsInjective <3>2. CASE /\ buffer = <<>> /\ Wait(waitSeqC, c) /\ UNCHANGED waitSeqP \* Get below so TLAPS knows about t \notin Range(waitSeqC) - BY <3>2, <2>2, AppendTransitivityIsInjective + BY <3>2, <2>2, AppendInjectiveSeq DEF Wait, IsInjective, Get <3>3. QED BY <2>2, <3>1, <3>2 DEF Get @@ -193,8 +194,14 @@ THEOREM Spec => BQS!Spec <3>2. CASE /\ Len(buffer) = BufCapacity /\ Wait(waitSeqP, p) /\ UNCHANGED waitSeqC - BY <2>1, <3>2 - DEF Wait, BQS!Next, BQS!vars, BQS!Put, BQS!Wait + <4>1. waitSeqP \in Seq(Producers) /\ waitSeqP' = Append(waitSeqP, p) + BY <3>2 DEF Wait, TypeInv + <4>2. Range(Append(waitSeqP, p)) = Range(waitSeqP) \cup {p} + BY <4>1, AppendProperties + <4>3. BQS!Put(p, p) + BY <2>1, <3>2, <4>1, <4>2 DEF Put, Wait, BQS!Put, BQS!Wait + <4>. QED + BY <2>1, <3>2, <4>3 DEF BQS!Next, BQS!vars, Wait <3>3. QED BY <2>1, <3>1, <3>2 DEF Put <2>2. ASSUME NEW c \in Consumers, @@ -217,7 +224,14 @@ THEOREM Spec => BQS!Spec <3>2. CASE /\ buffer = <<>> /\ Wait(waitSeqC, c) /\ UNCHANGED waitSeqP - BY <2>2, <3>2 DEF Wait, BQS!Next, BQS!vars, BQS!Get, BQS!Wait + <4>1. waitSeqC \in Seq(Consumers) /\ waitSeqC' = Append(waitSeqC, c) + BY <3>2 DEF Wait, TypeInv + <4>2. Range(Append(waitSeqC, c)) = Range(waitSeqC) \cup {c} + BY <4>1, AppendProperties + <4>3. BQS!Get(c) + BY <2>2, <3>2, <4>1, <4>2 DEF Get, Wait, BQS!Get, BQS!Wait + <4>. QED + BY <2>2, <3>2, <4>3 DEF BQS!Next, BQS!vars, Wait <3>3. QED BY <2>2, <3>1, <3>2 DEF Get <2>3. CASE UNCHANGED vars diff --git a/BlockingQueuePoisonApple_proofs.tla b/BlockingQueuePoisonApple_proofs.tla new file mode 100644 index 0000000..db71e4e --- /dev/null +++ b/BlockingQueuePoisonApple_proofs.tla @@ -0,0 +1,319 @@ +------------------- MODULE BlockingQueuePoisonApple_proofs ------------------ +(***************************************************************************) +(* TLAPS proofs for the BlockingQueuePoisonApple module. Kept in a *) +(* separate file so that the main specification stays free of TLAPS- *) +(* related INSTANCE statements and assumptions. *) +(* *) +(* Run with *) +(* tlapm --nofp -I /path/to/CommunityModules/modules *) +(* BlockingQueuePoisonApple_proofs.tla *) +(* so that the CommunityModules theorem files *) +(* (FunctionTheorems with SumFunction theorems) are visible to TLAPS. *) +(***************************************************************************) +EXTENDS BlockingQueuePoisonApple + +INSTANCE TLAPS +INSTANCE FiniteSetTheorems +INSTANCE SequenceTheorems +INSTANCE FunctionTheorems + +ASSUME FinAssumption == + /\ IsFiniteSet(Producers) + /\ IsFiniteSet(Consumers) + /\ Poison \notin Producers + +(***************************************************************************) +(* Step 1: TypeInv is itself inductive and is therefore a stand-alone *) +(* invariant of Spec . *) +(***************************************************************************) +LEMMA TypeInvInit == Init => TypeInv + BY Assumption, FinAssumption, FS_CardinalityType, EmptySeq DEF TypeInv, Init + +LEMMA TypeInvInductive == TypeInv /\ [Next]_vars => TypeInv' +<1> USE Assumption, FinAssumption, FS_CardinalityType + DEF TypeInv, vars, NotifyOther, Wait +<1> SUFFICES ASSUME TypeInv, [Next]_vars PROVE TypeInv' OBVIOUS +<1>1. ASSUME NEW p \in Producers, Put(p, p) PROVE TypeInv' + BY <1>1, AppendProperties DEF Put +<1>2. ASSUME NEW c \in Consumers, Get(c) PROVE TypeInv' + BY <1>2, HeadTailProperties DEF Get +<1>. QED BY <1>1, <1>2 DEF Next + +LEMMA TypeCorrect == Spec => []TypeInv + BY TypeInvInit, TypeInvInductive, PTL DEF Spec + +(***************************************************************************) +(* Step 2: NoDeadlock follows from a strengthened invariant DInv that *) +(* contains the two existential clauses guarding the empty / full buffer. *) +(***************************************************************************) +DInv == + /\ NoDeadlock + /\ (buffer = <<>>) => \E p \in Producers : p \notin waitSet + /\ (Len(buffer) = BufCapacity) => \E c \in Consumers : c \notin waitSet + +THEOREM Safety == Spec => []NoDeadlock +<1> USE Assumption, FinAssumption + DEF TypeInv, NoDeadlock, DInv, vars, Wait, NotifyOther +<1>1. Init => DInv BY EmptySeq DEF Init +<1>2. TypeInv /\ DInv /\ [Next]_vars => DInv' + <2> SUFFICES ASSUME TypeInv, DInv, [Next]_vars PROVE DInv' OBVIOUS + <2>1. ASSUME NEW p \in Producers, Put(p, p) PROVE DInv' BY <2>1 DEF Put + <2>2. ASSUME NEW c \in Consumers, Get(c) PROVE DInv' BY <2>2 DEF Get + <2>. QED BY <2>1, <2>2 DEF Next +<1>. QED BY <1>1, <1>2, TypeCorrect, PTL DEF Spec + +(***************************************************************************) +(* Step 3: QueueEmpty. Strengthen QueueEmpty into the inductive QInv: *) +(* (A) Cardinality(PoisonsInBuf) + SumFunction(prod) = SumFunction(cons).*) +(* The total of the remaining producer credits prod[p] plus the *) +(* number of Poison items in the buffer equals the total of the *) +(* remaining consumer credits cons[c] . *) +(* (B) FIFO ordering. Every non-Poison item in the buffer is followed *) +(* by a Poison further back, or some producer is still active. *) +(* Together (A) and (B) force buffer to be empty whenever ap = ac = {}. *) +(***************************************************************************) + +\* Index set of Poison occurrences in the buffer. +PoisonSet(buf) == { i \in 1..Len(buf) : buf[i] = Poison } +PoisonsInBuf == PoisonSet(buffer) + +QInv == + /\ Cardinality(PoisonsInBuf) + SumFunction(prod) = SumFunction(cons) + /\ \A i \in 1..Len(buffer) : buffer[i] # Poison => + (\E p \in Producers : prod[p] > 0) + \/ (\E j \in (i+1)..Len(buffer) : buffer[j] = Poison) + +(***************************************************************************) +(* Auxiliary lemmas about PoisonSet under Append and Tail. *) +(***************************************************************************) + +LEMMA PoisonSetFinite == + ASSUME NEW buf \in Seq(Producers \cup {Poison}) + PROVE IsFiniteSet(PoisonSet(buf)) + BY FS_Interval, FS_Subset DEF PoisonSet + +LEMMA PoisonAppendOther == + ASSUME NEW buf \in Seq(Producers \cup {Poison}), + NEW x \in Producers \cup {Poison}, x # Poison + PROVE PoisonSet(Append(buf, x)) = PoisonSet(buf) + BY AppendProperties, LenProperties DEF PoisonSet + +LEMMA PoisonAppendPoison == + ASSUME NEW buf \in Seq(Producers \cup {Poison}) + PROVE /\ PoisonSet(Append(buf, Poison)) = PoisonSet(buf) \cup {Len(buf) + 1} + /\ Cardinality(PoisonSet(Append(buf, Poison))) + = Cardinality(PoisonSet(buf)) + 1 +<1>1. PoisonSet(Append(buf, Poison)) = PoisonSet(buf) \cup {Len(buf) + 1} + BY AppendProperties, LenProperties DEF PoisonSet +<1>2. (Len(buf) + 1) \notin PoisonSet(buf) + BY LenProperties DEF PoisonSet +<1>. QED BY <1>1, <1>2, PoisonSetFinite, FS_AddElement + +LEMMA PoisonTail == + ASSUME NEW buf \in Seq(Producers \cup {Poison}), buf # <<>> + PROVE Cardinality(PoisonSet(Tail(buf))) + = Cardinality(PoisonSet(buf)) - (IF Head(buf) = Poison THEN 1 ELSE 0) +<1> USE FinAssumption +<1> DEFINE n == Len(buf) +<1> DEFINE Shift == { j \in 2..n : buf[j] = Poison } +<1>1. /\ Len(Tail(buf)) = n - 1 /\ n \in Nat /\ n >= 1 + /\ \A i \in 1..(n-1) : Tail(buf)[i] = buf[i + 1] + /\ Head(buf) = buf[1] + BY HeadTailProperties, LenProperties, EmptySeq +<1>2. IsFiniteSet(Shift) + BY FS_Interval, FS_Subset +<1>3. PoisonSet(Tail(buf)) = { i \in 1..(n - 1) : buf[i + 1] = Poison } + BY <1>1 DEF PoisonSet +<1>4. Cardinality(PoisonSet(Tail(buf))) = Cardinality(Shift) + <2> DEFINE f == [i \in PoisonSet(Tail(buf)) |-> i + 1] + <2>1. f \in Bijection(PoisonSet(Tail(buf)), Shift) + <3>1. f \in [PoisonSet(Tail(buf)) -> Shift] BY <1>3, <1>1 + <3>2. \A i, j \in PoisonSet(Tail(buf)) : f[i] = f[j] => i = j BY <1>3 + <3>3. \A k \in Shift : \E i \in PoisonSet(Tail(buf)) : f[i] = k + <4> SUFFICES ASSUME NEW k \in Shift + PROVE \E i \in PoisonSet(Tail(buf)) : f[i] = k + OBVIOUS + <4>1. (k - 1) \in PoisonSet(Tail(buf)) /\ f[k - 1] = k + BY <1>3, <1>1 + <4>. QED BY <4>1 + <3>. QED BY <3>1, <3>2, <3>3, Fun_IsBij + <2>2. IsFiniteSet(PoisonSet(Tail(buf))) + BY <1>3, <1>1, FS_Interval, FS_Subset + <2>. QED BY <2>1, <2>2, FS_Bijection DEF ExistsBijection +<1>5. CASE Head(buf) = Poison + <2>1. PoisonSet(buf) = Shift \cup {1} + <3> SUFFICES ASSUME NEW i \in 1..n + PROVE (buf[i] = Poison) <=> (i \in Shift \/ i = 1) + BY DEF PoisonSet + <3>. QED BY <1>1, <1>5 + <2>. QED BY <2>1, <1>4, <1>5, <1>2, FS_AddElement, FS_CardinalityType +<1>6. CASE Head(buf) # Poison + <2>1. PoisonSet(buf) = Shift + <3> SUFFICES ASSUME NEW i \in 1..n + PROVE (buf[i] = Poison) <=> i \in Shift + BY DEF PoisonSet + <3>. QED BY <1>1, <1>6 + <2>. QED BY <2>1, <1>4, <1>6, <1>2, FS_CardinalityType +<1>. QED BY <1>5, <1>6 + +(***************************************************************************) +(* The QInv components are well-typed. *) +(***************************************************************************) +LEMMA QInvTypes == + ASSUME TypeInv + PROVE /\ SumFunction(prod) \in Nat + /\ SumFunction(cons) \in Nat + /\ Cardinality(PoisonsInBuf) \in Nat + BY FinAssumption, FS_CardinalityType, SumFunctionNat, PoisonSetFinite + DEF TypeInv, PoisonsInBuf + +(***************************************************************************) +(* Main inductive proof. *) +(***************************************************************************) +THEOREM QueueEmptyTheorem == Spec => QueueEmpty +<1> DEFINE Inv == TypeInv /\ QInv +<1> USE Assumption, FinAssumption, FS_CardinalityType + DEF TypeInv, vars, NotifyOther, Wait, ap, ac, QueueEmpty, QInv +<1>1. Init => Inv + <2> SUFFICES ASSUME Init PROVE Inv OBVIOUS + <2>1. TypeInv BY EmptySeq DEF Init + <2>2. PoisonsInBuf = {} /\ Cardinality(PoisonsInBuf) = 0 + BY EmptySeq, FS_EmptySet DEF PoisonsInBuf, PoisonSet, Init + <2>3. SumFunction(prod) = Cardinality(Consumers) * Cardinality(Producers) + BY SumFunctionConst DEF Init + <2>4. SumFunction(cons) = Cardinality(Producers) * Cardinality(Consumers) + BY SumFunctionConst DEF Init + <2>. QED BY <2>1, <2>2, <2>3, <2>4, EmptySeq DEF Init +<1>2. Inv /\ [Next]_vars => Inv' + <2> SUFFICES ASSUME Inv, [Next]_vars PROVE Inv' OBVIOUS + <2>0. TypeInv' BY TypeInvInductive + <2> USE QInvTypes DEF Inv + <2>1. ASSUME NEW p \in Producers, Put(p, p) PROVE QInv' + <3> USE <2>1 + <3>0. /\ prod \in [Producers -> 0..Cardinality(Consumers)] + /\ buffer \in Seq(Producers \cup {Poison}) + /\ p \in Producers \cup {Poison} + /\ DOMAIN prod = Producers + BY DEF TypeInv + <3>1. CASE /\ Len(buffer) < BufCapacity + /\ buffer' = Append(buffer, p) + /\ UNCHANGED prod + /\ NotifyOther(Consumers) + /\ UNCHANGED <> + <4> USE <3>1 + <4>1. p # Poison BY DEF TypeInv + <4>2. PoisonsInBuf' = PoisonsInBuf + BY <4>1, <3>0, PoisonAppendOther DEF PoisonsInBuf + <4>3. \A i \in 1..Len(buffer') : buffer'[i] # Poison => + (\E q \in Producers : prod'[q] > 0) + \/ (\E j \in (i+1)..Len(buffer') : buffer'[j] = Poison) + BY DEF Put + <4>. QED BY <4>2, <4>3 + <3>2. CASE /\ Len(buffer) < BufCapacity + /\ buffer' = Append(buffer, Poison) + /\ prod' = [ prod EXCEPT ![p] = @ - 1] + /\ NotifyOther(Consumers) + /\ UNCHANGED <> + <4> USE <3>2 + <4>1. SumFunction(prod') = SumFunction(prod) - 1 + BY <3>0, SumFunctionExcept + <4>2. Cardinality(PoisonsInBuf') = Cardinality(PoisonsInBuf) + 1 + BY <3>0, PoisonAppendPoison DEF PoisonsInBuf + <4>3. \A i \in 1..Len(buffer') : buffer'[i] # Poison => + \E j \in (i+1)..Len(buffer') : buffer'[j] = Poison + <5> SUFFICES ASSUME NEW i \in 1..Len(buffer'), buffer'[i] # Poison + PROVE \E j \in (i+1)..Len(buffer') : buffer'[j] = Poison + OBVIOUS + <5>1. /\ Len(buffer') = Len(buffer) + 1 + /\ buffer'[Len(buffer) + 1] = Poison + BY AppendProperties, <3>0 + <5>2. (Len(buffer) + 1) \in (i+1)..Len(buffer') BY <5>1 + <5>. QED BY <5>1, <5>2 + <4>. QED BY <4>1, <4>2, <4>3 + <3>3. CASE /\ Len(buffer) = BufCapacity + /\ Wait(p) + /\ UNCHANGED prod + /\ UNCHANGED <> + BY <3>3 DEF Wait, PoisonsInBuf, PoisonSet + <3>. QED BY <3>1, <3>2, <3>3 DEF Put + <2>2. ASSUME NEW c \in Consumers, Get(c) PROVE QInv' + <3> USE <2>2 + <3>0. /\ cons \in [Consumers -> 0..Cardinality(Producers)] + /\ buffer \in Seq(Producers \cup {Poison}) + /\ DOMAIN cons = Consumers + BY DEF TypeInv + \* Helper for the FIFO part of QInv: when buffer' = Tail(buffer), any + \* non-Poison item in buffer' shifts down from a non-Poison item in + \* buffer that was witnessed by a Poison further back. + <3>F. ASSUME /\ buffer # <<>> + /\ buffer' = Tail(buffer) + /\ UNCHANGED prod + PROVE \A i \in 1..Len(buffer') : buffer'[i] # Poison => + (\E q \in Producers : prod'[q] > 0) + \/ (\E j \in (i+1)..Len(buffer') : buffer'[j] = Poison) + <4> USE <3>F + <4>1. /\ Len(buffer') = Len(buffer) - 1 + /\ \A k \in 1..Len(buffer') : buffer'[k] = buffer[k+1] + BY HeadTailProperties, <3>0 + <4> SUFFICES ASSUME NEW i \in 1..Len(buffer'), buffer'[i] # Poison + PROVE (\E q \in Producers : prod'[q] > 0) + \/ (\E j \in (i+1)..Len(buffer') : buffer'[j] = Poison) + OBVIOUS + <4>2. (i+1) \in 1..Len(buffer) /\ buffer[i+1] # Poison + BY <4>1 + <4>3. (\E q \in Producers : prod[q] > 0) + \/ (\E j \in (i+2)..Len(buffer) : buffer[j] = Poison) + BY <4>2 + <4>4. ASSUME NEW j \in (i+2)..Len(buffer), buffer[j] = Poison + PROVE \E j2 \in (i+1)..Len(buffer') : buffer'[j2] = Poison + <5>1. (j-1) \in (i+1)..Len(buffer') /\ buffer'[j-1] = buffer[j] + BY <4>1 + <5>. QED BY <5>1, <4>4 + <4>. QED BY <4>3, <4>4 + <3>1. CASE /\ buffer # <<>> + /\ buffer' = Tail(buffer) + /\ NotifyOther(Producers) + /\ Head(buffer) # Poison + /\ UNCHANGED <> + <4> USE <3>1 + <4>1. PoisonsInBuf' = PoisonSet(Tail(buffer)) BY DEF PoisonsInBuf + <4>2. Cardinality(PoisonsInBuf') = Cardinality(PoisonsInBuf) + BY <3>0, PoisonTail, <4>1 DEF PoisonsInBuf + <4>. QED BY <4>2, <3>F + <3>2. CASE /\ buffer # <<>> + /\ buffer' = Tail(buffer) + /\ NotifyOther(Producers) + /\ Head(buffer) = Poison + /\ cons' = [ cons EXCEPT ![c] = @ - 1] + /\ UNCHANGED <> + <4> USE <3>2 + <4>1. SumFunction(cons') = SumFunction(cons) - 1 + BY <3>0, SumFunctionExcept + <4>2. /\ PoisonsInBuf' = PoisonSet(Tail(buffer)) + /\ Cardinality(PoisonSet(Tail(buffer))) + = Cardinality(PoisonSet(buffer)) - 1 + BY <3>0, PoisonTail DEF PoisonsInBuf + <4>. QED BY <4>1, <4>2, <3>F DEF PoisonsInBuf + <3>3. CASE /\ buffer = <<>> + /\ Wait(c) + /\ UNCHANGED <> + BY <3>3 DEF Wait, PoisonsInBuf, PoisonSet + <3>. QED BY <3>1, <3>2, <3>3 DEF Get + <2>3. CASE UNCHANGED vars + BY <2>3 DEF PoisonsInBuf, PoisonSet + <2>. QED BY <2>0, <2>1, <2>2, <2>3 DEF Next +<1>3. Inv => (ap \cup ac = {} => buffer = <<>>) + <2> SUFFICES ASSUME Inv, ap \cup ac = {}, buffer # <<>> PROVE FALSE OBVIOUS + <2>1. /\ \A p \in Producers : prod[p] = 0 + /\ \A c \in Consumers : cons[c] = 0 + OBVIOUS + <2>2. SumFunction(prod) = 0 /\ SumFunction(cons) = 0 + BY <2>1, SumFunctionZero + <2>3. PoisonsInBuf = {} + BY <2>2, QInvTypes, FS_EmptySet, PoisonSetFinite DEF PoisonsInBuf + <2>4. 1 \in 1..Len(buffer) /\ buffer[1] # Poison + BY <2>3, EmptySeq DEF PoisonsInBuf, PoisonSet + <2>. QED BY <2>1, <2>3, <2>4 DEF PoisonsInBuf, PoisonSet +<1>. QED BY <1>1, <1>2, <1>3, PTL DEF Spec + +============================================================================= diff --git a/BlockingQueueSplit.tla b/BlockingQueueSplit.tla index afc10a0..798b1d4 100644 --- a/BlockingQueueSplit.tla +++ b/BlockingQueueSplit.tla @@ -101,4 +101,52 @@ THEOREM Implements == Spec => A!Spec A!vars, A!Put, A!Get, A!Wait, A!NotifyOther, A!RunningThreads <1>3. QED BY <1>1, <1>2, PTL, ITypeInv DEF Spec, A!Spec + +----------------------------------------------------------------------------- + +(* The IInv below mirrors the high-level BlockingQueue!IInv translated to *) +(* the split form: keep TypeInv!2 (Len) and the wait-set domain *) +(* constraints, the deadlock-freedom Invariant on the union, and the same *) +(* two existential clauses guarding the buffer = <<>> and full buffer *) +(* cases. *) +(* *) +(* Strictly speaking, proving DeadlockFreedom directly here is redundant: *) +(* the THEOREM Implements above already establishes Spec => A!Spec, hence *) +(* []A!Invariant transfers to BlockingQueueSplit by refinement. We prove *) +(* it locally as scaffolding/illustration of the inductive invariant. *) +IInv == + /\ Len(buffer) \in 0..BufCapacity + /\ waitSetP \in SUBSET Producers + /\ waitSetC \in SUBSET Consumers + /\ (waitSetC \cup waitSetP) # (Producers \cup Consumers) + /\ buffer = <<>> => \E p \in Producers : p \notin (waitSetC \cup waitSetP) + /\ Len(buffer) = BufCapacity => \E c \in Consumers : c \notin (waitSetC \cup waitSetP) + +(* This proof of deadlock freedom is self-contained: it only references *) +(* A!Invariant (the predicate) and never relies on BlockingQueue's *) +(* state machine (A!Init, A!Next, A!Spec) or its inductive invariant *) +(* A!IInv. *) +THEOREM DeadlockFreedom == Spec => []A!Invariant +<1> USE Assumption, ITypeInv DEF IInv, TypeInv, A!Invariant +<1>1. Init => IInv BY DEF Init +<1>2. TypeInv /\ IInv /\ [Next]_vars => IInv' + <2> SUFFICES ASSUME TypeInv, IInv, [Next]_vars + PROVE IInv' OBVIOUS + <2>1. ASSUME NEW p \in Producers, Put(p, p) + PROVE IInv' BY <2>1 DEF Put, Wait, NotifyOther, vars + <2>2. ASSUME NEW c \in Consumers, Get(c) + PROVE IInv' BY <2>2 DEF Get, Wait, NotifyOther, vars + <2>3. CASE UNCHANGED vars BY <2>3 DEF vars + <2>4. QED BY <2>1, <2>2, <2>3 DEF Next +<1>3. IInv => A!Invariant OBVIOUS +<1>4. QED BY <1>1, <1>2, <1>3, PTL DEF Spec + +(* IInv matches A!IInv up to splitting the wait-set constraint into its *) +(* Producers/Consumers components, hence implies it pointwise. Combined *) +(* with THEOREM Implements (Spec => A!Spec), this gives an alternative, *) +(* refinement-based route to deadlock freedom that does not require the *) +(* self-contained inductive proof of DeadlockFreedom above. *) +THEOREM IInvRefines == ASSUME IInv PROVE A!IInv + BY Assumption DEF IInv, A!IInv, A!TypeInv, A!Invariant + ============================================================================= diff --git a/CommunityModules.jar b/CommunityModules.jar deleted file mode 100644 index 1476eb3..0000000 Binary files a/CommunityModules.jar and /dev/null differ diff --git a/TLAPS.tla b/TLAPS.tla deleted file mode 100644 index d5f0473..0000000 --- a/TLAPS.tla +++ /dev/null @@ -1,311 +0,0 @@ -------------------------------- MODULE TLAPS -------------------------------- - -(* Backend pragmas. *) - - -(***************************************************************************) -(* Each of these pragmas can be cited with a BY or a USE. The pragma that *) -(* is added to the context of an obligation most recently is the one whose *) -(* effects are triggered. *) -(***************************************************************************) - -(***************************************************************************) -(* The following pragmas should be used only as a last resource. They are *) -(* dependent upon the particular backend provers, and are unlikely to have *) -(* any effect if the set of backend provers changes. Moreover, they are *) -(* meaningless to a reader of the proof. *) -(***************************************************************************) - - -(**************************************************************************) -(* Backend pragma: use the SMT solver for arithmetic. *) -(* *) -(* This method exists under this name for historical reasons. *) -(**************************************************************************) - -SimpleArithmetic == TRUE (*{ by (prover:"smt3") }*) - - -(**************************************************************************) -(* Backend pragma: SMT solver *) -(* *) -(* This method translates the proof obligation to SMTLIB2. The supported *) -(* fragment includes first-order logic, set theory, functions and *) -(* records. *) -(* SMT calls the smt-solver with the default timeout of 5 seconds *) -(* while SMTT(n) calls the smt-solver with a timeout of n seconds. *) -(**************************************************************************) - -SMT == TRUE (*{ by (prover:"smt3") }*) -SMTT(X) == TRUE (*{ by (prover:"smt3"; timeout:@) }*) - - -(**************************************************************************) -(* Backend pragma: CVC3 SMT solver *) -(* *) -(* CVC3 is used by default but you can also explicitly call it. *) -(**************************************************************************) - -CVC3 == TRUE (*{ by (prover: "cvc33") }*) -CVC3T(X) == TRUE (*{ by (prover:"cvc33"; timeout:@) }*) - -(**************************************************************************) -(* Backend pragma: Yices SMT solver *) -(* *) -(* This method translates the proof obligation to Yices native language. *) -(**************************************************************************) - -Yices == TRUE (*{ by (prover: "yices3") }*) -YicesT(X) == TRUE (*{ by (prover:"yices3"; timeout:@) }*) - -(**************************************************************************) -(* Backend pragma: veriT SMT solver *) -(* *) -(* This method translates the proof obligation to SMTLIB2 and calls veriT.*) -(**************************************************************************) - -veriT == TRUE (*{ by (prover: "verit") }*) -veriTT(X) == TRUE (*{ by (prover:"verit"; timeout:@) }*) - -(**************************************************************************) -(* Backend pragma: Z3 SMT solver *) -(* *) -(* This method translates the proof obligation to SMTLIB2 and calls Z3. *) -(**************************************************************************) - -Z3 == TRUE (*{ by (prover: "z33") }*) -Z3T(X) == TRUE (*{ by (prover:"z33"; timeout:@) }*) - -(**************************************************************************) -(* Backend pragma: SPASS superposition prover *) -(* *) -(* This method translates the proof obligation to the DFG format language *) -(* supported by the ATP SPASS. The translation is based on the SMT one. *) -(**************************************************************************) - -Spass == TRUE (*{ by (prover: "spass") }*) -SpassT(X) == TRUE (*{ by (prover:"spass"; timeout:@) }*) - -(**************************************************************************) -(* Backend pragma: The PTL propositional linear time temporal logic *) -(* prover. It currently is the LS4 backend. *) -(* *) -(* This method translates the negetation of the proof obligation to *) -(* Seperated Normal Form (TRP++ format) and checks for unsatisfiability *) -(**************************************************************************) - -LS4 == TRUE (*{ by (prover: "ls4") }*) -PTL == TRUE (*{ by (prover: "ls4") }*) - -(**************************************************************************) -(* Backend pragma: Zenon with different timeouts (default is 10 seconds) *) -(* *) -(**************************************************************************) - -Zenon == TRUE (*{ by (prover:"zenon") }*) -ZenonT(X) == TRUE (*{ by (prover:"zenon"; timeout:@) }*) - -(********************************************************************) -(* Backend pragma: Isabelle with different timeouts and tactics *) -(* (default is 30 seconds/auto) *) -(********************************************************************) - -Isa == TRUE (*{ by (prover:"isabelle") }*) -IsaT(X) == TRUE (*{ by (prover:"isabelle"; timeout:@) }*) -IsaM(X) == TRUE (*{ by (prover:"isabelle"; tactic:@) }*) -IsaMT(X,Y) == TRUE (*{ by (prover:"isabelle"; tactic:@; timeout:@) }*) - -(***************************************************************************) -(* The following theorem expresses the (useful implication of the) law of *) -(* set extensionality, which can be written as *) -(* *) -(* THEOREM \A S, T : (S = T) <=> (\A x : (x \in S) <=> (x \in T)) *) -(* *) -(* Theorem SetExtensionality is sometimes required by the SMT backend for *) -(* reasoning about sets. It is usually counterproductive to include *) -(* theorem SetExtensionality in a BY clause for the Zenon or Isabelle *) -(* backends. Instead, use the pragma IsaWithSetExtensionality to instruct *) -(* the Isabelle backend to use the rule of set extensionality. *) -(***************************************************************************) -IsaWithSetExtensionality == TRUE - (*{ by (prover:"isabelle"; tactic:"(auto intro: setEqualI)")}*) - -THEOREM SetExtensionality == \A S,T : (\A x : x \in S <=> x \in T) => S = T -OBVIOUS - -(***************************************************************************) -(* The following theorem is needed to deduce NotInSetS \notin SetS from *) -(* the definition *) -(* *) -(* NotInSetS == CHOOSE v : v \notin SetS *) -(***************************************************************************) -THEOREM NoSetContainsEverything == \A S : \E x : x \notin S -OBVIOUS (*{by (isabelle "(auto intro: inIrrefl)")}*) ------------------------------------------------------------------------------ - - - -(********************************************************************) -(********************************************************************) -(********************************************************************) - - -(********************************************************************) -(* Old versions of Zenon and Isabelle pragmas below *) -(* (kept for compatibility) *) -(********************************************************************) - - -(**************************************************************************) -(* Backend pragma: Zenon with different timeouts (default is 10 seconds) *) -(* *) -(**************************************************************************) - -SlowZenon == TRUE (*{ by (prover:"zenon"; timeout:20) }*) -SlowerZenon == TRUE (*{ by (prover:"zenon"; timeout:40) }*) -VerySlowZenon == TRUE (*{ by (prover:"zenon"; timeout:80) }*) -SlowestZenon == TRUE (*{ by (prover:"zenon"; timeout:160) }*) - - - -(********************************************************************) -(* Backend pragma: Isabelle's automatic search ("auto") *) -(* *) -(* This pragma bypasses Zenon. It is useful in situations involving *) -(* essentially simplification and equational reasoning. *) -(* Default imeout for all isabelle tactics is 30 seconds. *) -(********************************************************************) -Auto == TRUE (*{ by (prover:"isabelle"; tactic:"auto") }*) -SlowAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:120) }*) -SlowerAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:480) }*) -SlowestAuto == TRUE (*{ by (prover:"isabelle"; tactic:"auto"; timeout:960) }*) - -(********************************************************************) -(* Backend pragma: Isabelle's "force" tactic *) -(* *) -(* This pragma bypasses Zenon. It is useful in situations involving *) -(* quantifier reasoning. *) -(********************************************************************) -Force == TRUE (*{ by (prover:"isabelle"; tactic:"force") }*) -SlowForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:120) }*) -SlowerForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:480) }*) -SlowestForce == TRUE (*{ by (prover:"isabelle"; tactic:"force"; timeout:960) }*) - -(***********************************************************************) -(* Backend pragma: Isabelle's "simplification" tactics *) -(* *) -(* These tactics simplify the goal before running one of the automated *) -(* tactics. They are often necessary for obligations involving record *) -(* or tuple projections. Use the SimplfyAndSolve tactic unless you're *) -(* sure you can get away with just Simplification *) -(***********************************************************************) -SimplifyAndSolve == TRUE - (*{ by (prover:"isabelle"; tactic:"clarsimp auto?") }*) -SlowSimplifyAndSolve == TRUE - (*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:120) }*) -SlowerSimplifyAndSolve == TRUE - (*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:480) }*) -SlowestSimplifyAndSolve == TRUE - (*{ by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:960) }*) - -Simplification == TRUE (*{ by (prover:"isabelle"; tactic:"clarsimp") }*) -SlowSimplification == TRUE - (*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:120) }*) -SlowerSimplification == TRUE - (*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:480) }*) -SlowestSimplification == TRUE - (*{ by (prover:"isabelle"; tactic:"clarsimp"; timeout:960) }*) - -(**************************************************************************) -(* Backend pragma: Isabelle's tableau prover ("blast") *) -(* *) -(* This pragma bypasses Zenon and uses Isabelle's built-in theorem *) -(* prover, Blast. It is almost never better than Zenon by itself, but *) -(* becomes very useful in combination with the Auto pragma above. The *) -(* AutoBlast pragma first attempts Auto and then uses Blast to prove what *) -(* Auto could not prove. (There is currently no way to use Zenon on the *) -(* results left over from Auto.) *) -(**************************************************************************) -Blast == TRUE (*{ by (prover:"isabelle"; tactic:"blast") }*) -SlowBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:120) }*) -SlowerBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:480) }*) -SlowestBlast == TRUE (*{ by (prover:"isabelle"; tactic:"blast"; timeout:960) }*) - -AutoBlast == TRUE (*{ by (prover:"isabelle"; tactic:"auto, blast") }*) - - -(**************************************************************************) -(* Backend pragmas: multi-back-ends *) -(* *) -(* These pragmas just run a bunch of back-ends one after the other in the *) -(* hope that one will succeed. This saves time and effort for the user at *) -(* the expense of computation time. *) -(**************************************************************************) - -(* CVC3 goes first because it's bundled with TLAPS, then the other SMT - solvers are unlikely to succeed if CVC3 fails, so we run zenon and - Isabelle before them. *) -AllProvers == TRUE (*{ - by (prover:"cvc33") - by (prover:"zenon") - by (prover:"isabelle"; tactic:"auto") - by (prover:"spass") - by (prover:"smt3") - by (prover:"yices3") - by (prover:"verit") - by (prover:"z33") - by (prover:"isabelle"; tactic:"force") - by (prover:"isabelle"; tactic:"(auto intro: setEqualI)") - by (prover:"isabelle"; tactic:"clarsimp auto?") - by (prover:"isabelle"; tactic:"clarsimp") - by (prover:"isabelle"; tactic:"auto, blast") - }*) -AllProversT(X) == TRUE (*{ - by (prover:"cvc33"; timeout:@) - by (prover:"zenon"; timeout:@) - by (prover:"isabelle"; tactic:"auto"; timeout:@) - by (prover:"spass"; timeout:@) - by (prover:"smt3"; timeout:@) - by (prover:"yices3"; timeout:@) - by (prover:"verit"; timeout:@) - by (prover:"z33"; timeout:@) - by (prover:"isabelle"; tactic:"force"; timeout:@) - by (prover:"isabelle"; tactic:"(auto intro: setEqualI)"; timeout:@) - by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:@) - by (prover:"isabelle"; tactic:"clarsimp"; timeout:@) - by (prover:"isabelle"; tactic:"auto, blast"; timeout:@) - }*) - -AllSMT == TRUE (*{ - by (prover:"cvc33") - by (prover:"smt3") - by (prover:"yices3") - by (prover:"verit") - by (prover:"z33") - }*) -AllSMTT(X) == TRUE (*{ - by (prover:"cvc33"; timeout:@) - by (prover:"smt3"; timeout:@) - by (prover:"yices3"; timeout:@) - by (prover:"verit"; timeout:@) - by (prover:"z33"; timeout:@) - }*) - -AllIsa == TRUE (*{ - by (prover:"isabelle"; tactic:"auto") - by (prover:"isabelle"; tactic:"force") - by (prover:"isabelle"; tactic:"(auto intro: setEqualI)") - by (prover:"isabelle"; tactic:"clarsimp auto?") - by (prover:"isabelle"; tactic:"clarsimp") - by (prover:"isabelle"; tactic:"auto, blast") - }*) -AllIsaT(X) == TRUE (*{ - by (prover:"isabelle"; tactic:"auto"; timeout:@) - by (prover:"isabelle"; tactic:"force"; timeout:@) - by (prover:"isabelle"; tactic:"(auto intro: setEqualI)"; timeout:@) - by (prover:"isabelle"; tactic:"clarsimp auto?"; timeout:@) - by (prover:"isabelle"; tactic:"clarsimp"; timeout:@) - by (prover:"isabelle"; tactic:"auto, blast"; timeout:@) - }*) - -=============================================================================