dBFT 2.0 liveness issue #1
Conversation
tla/issue.md
Outdated
| @@ -0,0 +1,150 @@ | |||
| # dBFT 2.0 formal modelling and the liveness problem investigation | |||
tla/issue.md
Outdated
|
|
||
| ### Summary or problem description | ||
|
|
||
| This issue is aimed to emphasize the dBFT 2.0 liveness lock problem mentioned in |
tla/issue.md
Outdated
|
|
||
| This issue is aimed to emphasize the dBFT 2.0 liveness lock problem mentioned in | ||
| https://github.com/neo-project/neo/issues/2029#issuecomment-725612388 and in the | ||
| set of other related issues, PRs and papers with the help of TLA+ formal |
There was a problem hiding this comment.
mentioned in link and other discussions in issues and PRs. We've used TLA+ formal modeling tool to analyze dBFT 2.0 behaviour.
tla/issue.md
Outdated
| https://github.com/neo-project/neo/issues/2029#issuecomment-725612388 and in the | ||
| set of other related issues, PRs and papers with the help of TLA+ formal | ||
| modelling tool. In this issue we'll present the formal algorithm specification | ||
| and discuss the model checking results. |
There was a problem hiding this comment.
... specification with a set of identified problems and propose ways to fix them in so-called dBFT 2.1.
tla/issue.md
Outdated
| ### dBFT 2.0 formal models | ||
|
|
||
| We've created two models of dBFT 2.0 algorithm in TLA+. Please, visit the | ||
| [corresponding PR](https://github.com/nspcc-dev/dbft/pull/65), consider reading |
There was a problem hiding this comment.
Better (perma)link merged docs/files.
tla/issue.md
Outdated
| commit or do change view) completely depends on the message receiving order. | ||
|
|
||
| It should be noted that this kind of deadlock is possible in the 7-nodes network scenario | ||
| (TODO: run simple model with 7 good nodes). Moreover, we've faced with exactly this kind |
There was a problem hiding this comment.
I doubt 4-7 should be mentioned, it's the same protocol with the same basic behavior.
AnnaShaleva
force-pushed
the
issue
branch
2 times, most recently
from
4c23da1 to
5fbc016
Compare
tla/issue.md
Outdated
| ### Further work | ||
|
|
||
| The whole idea of TLA+ dBFT modelling was to reveal and avoid the liveness lock | ||
| problems so that we've got a troubleproofly operating consensus algorithm in our |
tla/issue.md
Outdated
| 1. Collect and process the community feedback on proposed TLA+ dBFT 2.0 and 2.1 | ||
| specifications, fix the models (in case of any bugs found). | ||
| 2. Implement the improved dBFT 2.1 algorithm at the code level. | ||
| 3. Create TLA+ specification and investigate liveness problems of the dBFT 3.0 |
tla/issue.md
Outdated
| any model deadlock: the malicious node keep sending messages if possible to escape | ||
| from the liveness lock. Moreover, the presence of faulty nodes significantly | ||
| increases the states graph size, so that it takes quite a long time to evaluate | ||
| the whole set of possible model behaviours. |
There was a problem hiding this comment.
Haven't we checked this completely?
There was a problem hiding this comment.
Yes, we have for both scenarious when primary and non-primary is faulty. So I probably have to remove the last sentence.
There was a problem hiding this comment.
Actually, I still have doubts about it and not sure whether it works correctly. I really expected this faulty model to end up in a deadlock.
There was a problem hiding this comment.
I've rephrased this sentence, see the latest commit.
models: add dBFT 2.1 models
No description provided.