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

models: adjust MoreThanFNodesCommitted check #2

Merged
merged 1 commit into from
Mar 14, 2023
Merged

models: adjust MoreThanFNodesCommitted check #2

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 12 additions & 4 deletions formal-models/dbft/dbft.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,11 +103,19 @@ GetPrimary(view) == CHOOSE r \in RM : view % N = r
GetNewView(oldView) == oldView + 1

\* CountCommitted returns the number of nodes that have sent the Commit message
\* in the current round (as the node r sees it).
CountCommitted(r) == Cardinality({rm \in RM : Cardinality({msg \in msgs : msg.rm = rm /\ msg.type = "Commit" /\ msg.view = rmState[r].view}) /= 0})
\* in the current round or in some other round.
CountCommitted(r) == Cardinality({rm \in RM : Cardinality({msg \in msgs : msg.rm = rm /\ msg.type = "Commit"}) /= 0})
roman-khimov marked this conversation as resolved.
Show resolved Hide resolved

\* MoreThanFNodesCommitted returns whether more than F nodes have been committed
\* in the current round (as the node r sees it).
\*
\* IMPORTANT NOTE: we intentionally do not add the "lost" nodes calculation to the specification, and here's
\* the reason: from the node's point of view we can't reliably check that some neighbour is completely
\* out of the network. It is possible that the node doesn't receive consensus messages from some other member
\* due to network delays. On the other hand, real nodes can go down at any time. The absence of the
\* member's message doesn't mean that the member is out of the network, we never can be sure about
\* that, thus, this information is unreliable and can't be trusted during the consensus process.
\* What can be trusted is whether there's a Commit message from some member was received by the node.
MoreThanFNodesCommitted(r) == CountCommitted(r) > F

\* PrepareRequestSentOrReceived denotes whether there's a PrepareRequest
Expand Down Expand Up @@ -147,7 +155,7 @@ RMSendPrepareResponse(r) ==
\* condition specifies only the thing that may happen given some particular set of enabling conditions.
\* Thus, we've extended the NotAcceptingPayloadsDueToViewChanging condition to consider only MoreThanFNodesCommitted.
\* It should be noted that the logic of MoreThanFNodesCommittedOrLost can't be reliable in detecting lost nodes
\* (even with neo-project/neo#2057), because real nodes can go down at any time.
\* (even with neo-project/neo#2057), because real nodes can go down at any time. See the comment above the MoreThanFNodesCommitted.
\/ /\ rmState[r].type = "cv"
/\ MoreThanFNodesCommitted(r)
/\ \neg IsPrimary(r)
Expand Down Expand Up @@ -374,7 +382,7 @@ THEOREM Spec => [](TypeOK /\ InvTwoBlocksAccepted /\ InvFaultNodesCount)

=============================================================================
\* Modification History
\* Last modified Mon Feb 27 16:46:19 MSK 2023 by root
\* Last modified Mon Mar 06 15:36:57 MSK 2023 by root
\* Last modified Fri Feb 17 15:47:41 MSK 2023 by anna
\* Last modified Sat Jan 21 01:26:16 MSK 2023 by rik
\* Created Thu Dec 15 16:06:17 MSK 2022 by anna