Skip to content
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.

Sign up for GitHub

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

Jump to bottom

TLA+ model for enhanced Bane dBFT with an additional phase #111

Closed
roman-khimov opened this issue Apr 1, 2024 · 0 comments · Fixed by #116
Closed

TLA+ model for enhanced Bane dBFT with an additional phase #111

roman-khimov opened this issue Apr 1, 2024 · 0 comments · Fixed by #116
Assignees
@AnnaShaleva
Labels
feature Completely new functionality I2 Regular impact S1 Highly significant U2 Seriously planned
Milestone
v0.3.0

Comments

@roman-khimov
Copy link
Member

Is your feature request related to a problem? Please describe.

I'm always frustrated when we don't have a model for the protocol we're going to use.

Describe the solution you'd like

Bane will need an additional phase, let's try it in TLA+ first to ensure it has the same properties as we have with dBFT 2.0.
@roman-khimov roman-khimov added U2 Seriously planned S1 Highly significant I2 Regular impact feature Completely new functionality labels Apr 1, 2024
@roman-khimov roman-khimov mentioned this issue Apr 1, 2024
Closed
@AnnaShaleva AnnaShaleva added this to the v0.3.0 milestone Apr 25, 2024
AnnaShaleva added a commit that referenced this issue Apr 25, 2024
@AnnaShaleva
formal-models: extend dBFT with additional post-commit phase
7125076 
Close #111.

Signed-off-by: Anna Shaleva <shaleva.ann@nspcc.ru>
@AnnaShaleva AnnaShaleva mentioned this issue Apr 25, 2024
Merged
4 tasks
AnnaShaleva added a commit that referenced this issue Jun 20, 2024
@AnnaShaleva
formal-models: extend dBFT with additional post-commit phase
2b6c4cf 
Close #111. The additional step is called RMSendAck and allows to send
Ack message once enough Commit messages are received. Block can be
accepted only if BFT number of Ack messages are collected.

Signed-off-by: Anna Shaleva <shaleva.ann@nspcc.ru>
AnnaShaleva added a commit that referenced this issue Jun 20, 2024
@AnnaShaleva
formal-models: extend dBFT with additional post-commit phase
0095b94 
Close #111. The additional step is called RMSendAck and allows to send
Ack message once enough Commit messages are received. Block can be
accepted only if BFT number of Ack messages are collected.

Signed-off-by: Anna Shaleva <shaleva.ann@nspcc.ru>
AnnaShaleva added a commit that referenced this issue Jun 20, 2024
@AnnaShaleva
formal-models: extend dBFT with additional post-commit phase
847c944 
Close #111. The additional step is called RMSendAck and allows to send
Ack message once enough Commit messages are received. Block can be
accepted only if BFT number of Ack messages are collected.

Signed-off-by: Anna Shaleva <shaleva.ann@nspcc.ru>
AnnaShaleva added a commit that referenced this issue Jun 21, 2024
@AnnaShaleva
formal-models: extend dBFT with additional post-commit phase
5124528 
Close #111. The additional step is called RMSendAck and allows to send
Ack message once enough Commit messages are received. Block can be
accepted only if BFT number of Ack messages are collected.

Signed-off-by: Anna Shaleva <shaleva.ann@nspcc.ru>
AnnaShaleva added a commit that referenced this issue Jun 24, 2024
@AnnaShaleva
formal-models: extend dBFT with additional post-commit phase
de50c7b 
Close #111. The additional step is called RMSendAck and allows to send
Ack message once enough Commit messages are received. Block can be
accepted only if BFT number of Ack messages are collected.

Signed-off-by: Anna Shaleva <shaleva.ann@nspcc.ru>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@AnnaShaleva AnnaShaleva

Labels
feature Completely new functionality I2 Regular impact S1 Highly significant U2 Seriously planned
Projects
None yet
Milestone
v0.3.0
Development

Successfully merging a pull request may close this issue.

formal-models: extend dBFT with additional post-commit phase nspcc-dev/dbft
2 participants
@roman-khimov @AnnaShaleva