-
Notifications
You must be signed in to change notification settings - Fork 14
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
spec: Overview over consensus logic covered with tests (#92)
* Overview over consensus logic covered with tests * added pending logic for prevote value * fixed all tests * line 28 test * nice parameterized testrun * DSL * 7 process test and assertion * Added a test to reach line 42 without locking * Use `--max-samples 100` for Quint tests --------- Co-authored-by: Romain Ruetschi <[email protected]>
- Loading branch information
1 parent
a733850
commit 1074875
Showing
13 changed files
with
303 additions
and
28 deletions.
There are no files selected for viewing
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
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,52 @@ | ||
| // -*- mode: Bluespec; -*- | ||
|
|
||
| module TendermintDSL { | ||
|
|
||
| import statemachineAsync.* from "./statemachineAsync" | ||
| export statemachineAsync.* | ||
|
|
||
| val validatorList = validators.fold(List(), (s, x) => s.append(x)) | ||
| val correctList = Correct.fold(List(), (s, x) => s.append(x)) | ||
| val faultyList = Faulty.fold(List(), (s, x) => s.append(x)) | ||
|
|
||
| run ListTakeAStep (active) = { | ||
| active.length().reps(i => valStep(active[i])) | ||
| } | ||
|
|
||
| run ListDeliverProposal (active, proposalMsg) = { | ||
| active.length().reps(i => deliverProposal(active[i], proposalMsg)) | ||
| } | ||
|
|
||
| run ListDeliverSomeProposal (active) = { | ||
| active.length().reps(i => deliverSomeProposal(active[i])) | ||
| } | ||
|
|
||
| run ProcessDeliverAllVotes (cstep, recepient, fromList, valset, h, r, value) = { | ||
| fromList.length().reps(i => deliverVote(recepient, { src: fromList[i], height: h, round: r, step: cstep, id: value })) | ||
| } | ||
|
|
||
| run ListDeliverAllVotes (cstep, fromList, toList, valset, h, r, value) = { | ||
| toList.length().reps(i => ProcessDeliverAllVotes (cstep, toList[i], fromList, valset, h, r, value)) | ||
| } | ||
|
|
||
|
|
||
| run everyoneReceivesProposal (active, valList, valset, h, r, value) = { | ||
| val p = Proposer (valset, h, r) | ||
| setNextValueToPropose(p, value) | ||
| .then(ListTakeAStep(active)) | ||
| .then(all { | ||
| assert(true), | ||
| ListDeliverSomeProposal(active) | ||
| }) | ||
| .then(ListTakeAStep(active)) | ||
| } | ||
|
|
||
| run fromPrevoteToPrecommit (prevoteSenders, prevoteReceivers, valList, valset, h, r, value) = { | ||
| ListDeliverAllVotes("Prevote", prevoteSenders, prevoteReceivers, valset, h, r, value) | ||
| .then(prevoteSenders.length().reps(_ => ListTakeAStep(prevoteReceivers))) | ||
| // extra step due to timeoutprevote double step | ||
| .then(ListTakeAStep(prevoteReceivers)) | ||
| } | ||
|
|
||
|
|
||
| } |
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,43 @@ | ||
| # Tests for consensus statemachine (and sometimes driver) | ||
|
|
||
| ## Overview over covered consensus algorithm lines | ||
|
|
||
| | line | comment | (C) | test | | ||
| | -----:| ---- | -----| -----| | ||
| 16 | reuse valid value | | line28Test.qnt | ||
| 18 | new value | X2 | ||
| 19 | send proposal | | (A) RoundswitchTest (^1) | ||
| 21 | start timeoutPropose | X1, X2b, X2c | ||
| 24 | prevote value | X1, X2 | ||
| 26 | prevote nil (on invalid or locked) | X2c | ||
| 30 | prevote value on old prevotes | | line28Test.qnt | ||
| 32 | prevote nil on old prevotes (on invalid or locked) | | ||
| 35 | start timeoutPrevote | X2 | ||
| 40 | precommit value | X1 | ||
| 42 without 41 | set valid without locked | | line42Test | ||
| 45 | precommit nil | X2b | ||
| 48 | start timeoutPrecommit | X2 , X2b | ||
| 51 | decide | X1 | ||
| 56 | skip round | | (A) RoundswitchTest | ||
| 57 | OnTimeoutPropose | X2b | ||
| 61 | OnTimeOutPrevote | X2 | ||
| 64 | OnTimeOutPrecommit | X2, X2b | ||
|
|
||
| ## Comments | ||
|
|
||
| - (C) | ||
| - refers to DecideNonProposerTest in consensusTest.qnt. | ||
| - X1 covered in height 1, X2b: covered in height 2 round 2, etc. | ||
| - is only containing the consensus state machine. No driver | ||
| - contains an event to go to height 1 | ||
| - (A) asyncModelsTest.qnt | ||
| - ^1 ThreeDecideInRound1V4stillinZeroTest delivers proposal so it must have been sent before | ||
|
|
||
|
|
||
| ## Other tests | ||
|
|
||
| - asyncModelsTest.qnt | ||
| - DisagreementTest: 2/4 faulty lead to disagreement | ||
| - three processes go to round 1 and decide, on process left behind. Test whether process decides | ||
| - DecideForFutureRoundTest: first receives proposal then precommits | ||
| - DecideOnProposalTest: first receives precommits then proposal |
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,34 @@ | ||
| // -*- mode: Bluespec; -*- | ||
|
|
||
| module line28Test { | ||
|
|
||
| import line28run( | ||
| validators = Set("v1", "v2", "v3", "v4"), | ||
| validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), | ||
| Faulty = Set("v1"), | ||
| Values = Set("red", "blue"), | ||
| Rounds = Set(0, 1, 2, 3), | ||
| Heights = Set(0), // , 1, 2, 3) | ||
| otherSet = Set("v2", "v4") | ||
| ) as N4F1 from "./line28run" | ||
|
|
||
| run line28Test = { | ||
| N4F1::runToLine28 | ||
| } | ||
|
|
||
| import line28run( | ||
| validators = Set("v1", "v2", "v3", "v4", "v5", "v6", "v7"), | ||
| validatorSet = Set("v1", "v2", "v3", "v4", "v5", "v6", "v7").mapBy(x => 1), | ||
| Faulty = Set("v1"), | ||
| Values = Set("red", "blue"), | ||
| Rounds = Set(0, 1, 2, 3), | ||
| Heights = Set(0), // , 1, 2, 3) | ||
| otherSet = Set("v2", "v4", "v6", "v7") | ||
| ) as N7F1 from "./line28run" | ||
|
|
||
| run Bigline28Test = { | ||
| N7F1::runToLine28 | ||
| } | ||
|
|
||
|
|
||
| } |
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,40 @@ | ||
| // -*- mode: Bluespec; -*- | ||
|
|
||
| module line28run { | ||
|
|
||
| import TendermintDSL.* from "./TendermintDSL" | ||
| export TendermintDSL.* | ||
|
|
||
| const otherSet : Set[Address_t] | ||
| val others = otherSet.fold(List(), (s, x) => s.append(x)) | ||
|
|
||
| run runToLine28 = { | ||
| val nextProposer = Proposer (validatorSet, 0, 1) | ||
| init | ||
| .then(all { | ||
| // others should be at most 2/3. | ||
| // if this assertion fails the set need to be set differently | ||
| assert(3 * size(otherSet) <= 2 * size(validators)), | ||
| assert(3 * size(otherSet.union(Faulty)) > 2 * size(validators)), | ||
| everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 0, "blue") | ||
| }) | ||
| // receive all prevotes | ||
| .then(fromPrevoteToPrecommit (correctList, correctList, validatorList, validatorSet, 0, 0, "blue")) | ||
| // now the faulty nodes precommit nil | ||
| .then(ListDeliverAllVotes("Precommit", faultyList, correctList, validatorSet, 0, 0, "nil")) | ||
| .then(faultyList.length().reps(_ => ListTakeAStep(correctList))) | ||
| // now the other precommits are delivered, so that timeoutPrecommit is started | ||
| .then(ListDeliverAllVotes("Precommit", others, correctList, validatorSet, 0, 0, "blue")) | ||
| .then(others.length().reps(_ => ListTakeAStep(correctList))) | ||
| // TimeoutPrecommit is there an can fire and bring is to the next round. | ||
| .then(all{ | ||
| assert(system.get(nextProposer).timeout.contains(("TimeoutPrecommit", 0, 0))), | ||
| everyoneReceivesProposal(correctList, validatorList, validatorSet, 0, 0, "red") | ||
| }) | ||
| .then(all{ | ||
| assert(voteBuffer.get(nextProposer).contains( { height: 0, id: "blue", round: 1, src: nextProposer, step: "Prevote" })), | ||
| unchangedAll | ||
| }) | ||
| } | ||
|
|
||
| } |
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,19 @@ | ||
| // -*- mode: Bluespec; -*- | ||
|
|
||
| module line42Test { | ||
|
|
||
| import line42run( | ||
| validators = Set("v1", "v2", "v3", "v4"), | ||
| validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), | ||
| Faulty = Set(), | ||
| Values = Set("red", "blue"), | ||
| Rounds = Set(0, 1, 2, 3), | ||
| Heights = Set(0), // , 1, 2, 3) | ||
| testedVal = "v4" | ||
| ) as N4F0 from "./line42run" | ||
|
|
||
| run line42Test = { | ||
| N4F0::runToLine42 | ||
| } | ||
|
|
||
| } |
Oops, something went wrong.