-
Notifications
You must be signed in to change notification settings - Fork 12
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
spec: Add skip round logic #75
Merged
Merged
Changes from 11 commits
Commits
Show all changes
19 commits
Select commit
Hold shift + click to select a range
3882d89
start skip round logic (missing to see what messages are there upon s…
josef-widder 4461d77
added skip round reaction upon votes
josef-widder 1faa209
bug in strings calling bookkeeper fixed
josef-widder f511c80
another wrong string
josef-widder 0ce7930
added round switch test - not activated yet
josef-widder c25c1aa
tests around round switching
josef-widder 6fcfaf8
failing test
josef-widder 1662d0f
Fix typos
romac 293f857
added a test that generates a lot of unsuccessful rounds
josef-widder 26e590d
Merge branch 'josef/skipRoundLogic' of github.com:informalsystems/mal…
josef-widder 1fb7028
added assertion for correct round
josef-widder b71cbcc
Ensure `Skip` event is emitted even when no threshold has been reache…
romac fac95fe
Ensure `Skip` event is emitted only when vote round is strictly great…
romac 03bbb3d
Remove debug statement
romac cdef7ba
parameterized test is more concise
josef-widder 1724815
Merge branch 'josef/skipRoundLogic' of github.com:informalsystems/mal…
josef-widder a08455f
made parameterized test even more concise
josef-widder f5a124b
added an assertion at the end of unsuccessful round
josef-widder a6a1281
Merge branch 'main' into josef/skipRoundLogic
romac File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
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,95 @@ | ||
| module parameterizedTest { | ||
|
|
||
| import statemachineAsync( | ||
| validators = Set("v1", "v2", "v3", "v4"), | ||
| validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), | ||
| Faulty = Set(), | ||
| Values = Set("a", "b"), | ||
| Rounds = Set(0, 1, 2, 3), | ||
| Heights = Set(0) // , 1, 2, 3) | ||
| ) as N4F0 from "./statemachineAsync" | ||
|
|
||
|
|
||
| // run everyoneTakesAStep (proposer, nonprop) = { | ||
| // N4F0::valStep(nonprop._1) | ||
| // .then(N4F0::valStep(nonprop._2)) | ||
| // .then(N4F0::valStep(nonprop._3)) | ||
| // .then(N4F0::valStep(proposer)) | ||
| // } | ||
|
|
||
| run everyoneTakesAStep = { | ||
| N4F0::valStep("v1") | ||
| .then(N4F0::valStep("v2")) | ||
| .then(N4F0::valStep("v3")) | ||
| .then(N4F0::valStep("v4")) | ||
| } | ||
|
|
||
| run oneDeliversPrevote (validator, prop, r, proposer, nonprop) = { | ||
| N4F0::deliverVote(validator, { height: 0, id: "nil", round: r, src: nonprop._1, step: "Prevote" }) | ||
| .then(N4F0::deliverVote(validator, { height: 0, id: "nil", round: r, src: nonprop._2, step: "Prevote" })) | ||
| .then(N4F0::deliverVote(validator, { height: 0, id: "nil", round: r, src: nonprop._3, step: "Prevote" })) | ||
| .then(N4F0::deliverVote(validator, { height: 0, id: prop, round: r, src: proposer, step: "Prevote" })) | ||
| } | ||
|
|
||
| run oneDeliversPrecommit (validator, prop, r, proposer, nonprop) = { | ||
| N4F0::deliverVote(validator, { height: 0, id: "nil", round: r, src: nonprop._1, step: "Precommit" }) | ||
| .then(N4F0::deliverVote(validator, { height: 0, id: "nil", round: r, src: nonprop._2, step: "Precommit" })) | ||
| .then(N4F0::deliverVote(validator, { height: 0, id: "nil", round: r, src: nonprop._3, step: "Precommit" })) | ||
| .then(N4F0::deliverVote(validator, { height: 0, id: "nil", round: r, src: proposer, step: "Precommit" })) | ||
| } | ||
|
|
||
| run UnSuccessfulRound (prop: str, r: int) : bool = { | ||
| val proposer = N4F0::Proposer(N4F0::validatorSet, 0, r) | ||
| val nonprop = if (proposer == "v1") ("v2", "v3", "v4") | ||
| else if (proposer == "v2") ("v1", "v3", "v4") | ||
| else if (proposer == "v3") ("v1", "v2", "v4") | ||
| else ("v1", "v2", "v3") | ||
| // everyone is in round r and proposer sent a proposal | ||
| all { | ||
| assert(N4F0::propBuffer.keys().forall(p => N4F0::propBuffer.get(p).contains( | ||
| { height: 0, proposal: prop, round: r, src: proposer, validRound: -1 }) )), | ||
| N4F0::unchangedAll | ||
| } | ||
| .then(N4F0::deliverProposal(proposer, { height: 0, proposal: prop, round: r, src: proposer, validRound: -1 })) | ||
| .then(everyoneTakesAStep) | ||
| .then(oneDeliversPrevote(proposer, prop, r, proposer, nonprop)) | ||
| .then(oneDeliversPrevote(nonprop._1, prop, r, proposer, nonprop)) | ||
| .then(oneDeliversPrevote(nonprop._2, prop, r, proposer, nonprop)) | ||
| .then(oneDeliversPrevote(nonprop._3, prop, r, proposer, nonprop)) | ||
| .then(everyoneTakesAStep) | ||
| .then(everyoneTakesAStep) | ||
| .then(everyoneTakesAStep) | ||
| .then(all { | ||
| assert(N4F0::system.keys().forall(p => N4F0::system.get(p).timeout.contains( | ||
| ("TimeoutPrevote", 0, r)) )), | ||
| N4F0::unchangedAll | ||
| }) | ||
| .then(everyoneTakesAStep) | ||
| .then(oneDeliversPrecommit(proposer, prop, r, proposer, nonprop)) | ||
| .then(oneDeliversPrecommit(nonprop._1, prop, r, proposer, nonprop)) | ||
| .then(oneDeliversPrecommit(nonprop._2, prop, r, proposer, nonprop)) | ||
| .then(oneDeliversPrecommit(nonprop._3, prop, r, proposer, nonprop)) | ||
| .then(everyoneTakesAStep) | ||
| .then(everyoneTakesAStep) | ||
| .then(everyoneTakesAStep) | ||
| .then(everyoneTakesAStep) | ||
| } | ||
|
|
||
| run UnSuccessfulRoundWithSetup (prop: str, r: int) : bool = { | ||
| N4F0::setNextValueToPropose(N4F0::Proposer(N4F0::validatorSet, 0, r), prop) | ||
| .then(everyoneTakesAStep) | ||
| .then(all { | ||
| assert(N4F0::system.keys().forall(p => N4F0::system.get(p).es.cs.round == r)), | ||
| UnSuccessfulRound (prop, r) | ||
| }) | ||
| } | ||
|
|
||
| run multiRoundTest = { | ||
| val proposals = ["blue", "red", "green", "yellow"] | ||
| val repetitions = proposals.length() | ||
| N4F0::init | ||
| .then(repetitions.reps(i => UnSuccessfulRoundWithSetup(proposals[i], i))) | ||
| } | ||
|
|
||
|
|
||
| } |
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@romac could you please have a look here. This test fails, although as far as I understand if the bookkeeper would generate the skip event properly, it should go through. Here v4
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah that sounds right. But the test appears to be passing, or am I misunderstanding what the test is checking?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Weird, locally it doesn't. Perhaps I have messed something up with branches locally. If the test passes, let's not block on this, and we can have a look (and add more tests later)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It does pass locally for me either. Not sure what happened with the CI but let's trust our eyes for now. I'll look into it!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can it be due to non-determinism? We might have gotten lucky on the CI this one time.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah I added the check while I was writing the comment.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you please expand on that? I am not sure I am following what you are getting at.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It was just an observation that in the interface between the bookkeeper and the executor, we most of time don't need to pass the current round. That is, only for generating the skip rule we actually need the current round, while for the rest of the bookkeeper logic, the round that is passed as part of the vote is sufficient. Perhaps it is not important, it was just for me to understand ;-)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah gotcha! Yeah it's a shame this is the only case where we need the current round, maybe this hints at a better way to model the code and decouple things further but I am not seeing it right now. If the current state of things is fine with you then let's leave it at that for now?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, we can leave it for now.
If I think longer about it, the current solution also becomes more natural: the consensus algorithm forces us to ignore the current round in several places. In the arXiv paper
So actually, perhaps it is natural that most of the time we don't care about the current round when doing bookkeeping. So perhaps it is just intuition that is failing me here: while we think about messages from the current round a lot for lucky path, etc., the mentioned lines require us to look at messages from all rounds.
So, I guess it is good. Again, thanks for fixing the issue!