spec: Add skip round logic #75
Conversation
|
I just merged #74 |
@josef-widder Do you want to address this in this PR, or do it in a follow-up PR? |
Specs/Quint/asyncModelsTest.qnt
Outdated
| // this should work, once the bookkeeper skip event is fixed | ||
| assert(N4F0::system.get("v4").es.cs.round == 1), |
There was a problem hiding this comment.
@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
- lags behind in round 0
- then receives 3 round 1 messages (two precommits and one prevote). The messages are stored in the bookkeeper
- at some point a skip event should bring v4 to round 1 but it never happens
There was a problem hiding this comment.
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.
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.
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.
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.
Just to be sure. This is the check <...> that you already added, right?
Yeah I added the check while I was writing the comment.
There was a problem hiding this comment.
But the point is that even if the votekeeper generates events for round less than the current round, the executor has to figure out whether it still wants to do in some rounds (and sometimes does).
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.
I am not sure I am following what you are getting at.
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.
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.
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
- for line 28 we may need prevotes from the previous round,
- for line 49 we may need precommits from previous (in fact any) rounds.
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!
I think there is nothing to be done if the skip works correctly. if we skip on the f+1st message, no messages can be around. If we skip on 2f+1 I think it is also fine, but I can have a look and do a follow-up PR if necessary. But there is the failing test I just mentioned a minute ago. |
…achite into josef/skipRoundLogic
…er than the current round
…achite into josef/skipRoundLogic
I guess I will need to wait until we merge #74 until I can finish completing it. (In the current version, the votekeeper does not produce the proper skip event)