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

docs: updating tla+ spec #641

Merged
merged 6 commits into from
Aug 21, 2023
Merged

docs: updating tla+ spec #641

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
36d071d
chore: updating consensus spec
b00f Aug 19, 2023
8e6ac92
chore: updating pdf file
b00f Aug 19, 2023
957e514
docs: reducing cp_round by -1
b00f Aug 20, 2023
1d54885
Merge branch 'main' into tla+-update
themantre Aug 20, 2023
1fb44c8
Merge branch 'main' into tla+-update
b00f Aug 21, 2023
66263b9
Merge branch 'main' into tla+-update
b00f Aug 21, 2023
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
1 change: 1 addition & 0 deletions consensus/spec/Pactus.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ CONSTANTS
FaultyNodes = {3}
MaxHeight = 1
MaxRound = 1
MaxCPRound = 1

INVARIANT TypeOK
PROPERTY Success
Binary file modified consensus/spec/Pactus.pdf
View file
Open in desktop
Binary file not shown.
58 changes: 31 additions & 27 deletions consensus/spec/Pactus.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ ASSUME

\* Fetch a subset of messages in the network based on the params filter.
SubsetOfMsgs(params) ==
{msg \in log: \A field \in DOMAIN params: msg[field] = params[field]}
{msg \in log: \A field \in DOMAIN params: msg[field] = params[field]}

\* IsProposer checks if the replica is the proposer for this round.
\* To simplify, we assume the proposer always starts with the first replica,
Expand Down Expand Up @@ -121,14 +121,6 @@ CPHasOneMainVotesZeroInPrvRound(index) ==
cp_round |-> states[index].cp_round - 1,
cp_val |-> 0])) > 0

CPHasOneThirdMainVotesOneInPrvRound(index) ==
Cardinality(SubsetOfMsgs([
type |-> "CP:MAIN-VOTE",
height |-> states[index].height,
round |-> states[index].round,
cp_round |-> states[index].cp_round - 1,
cp_val |-> 1])) >= OneThird

CPHasOneMainVotesOneInPrvRound(index) ==
Cardinality(SubsetOfMsgs([
type |-> "CP:MAIN-VOTE",
Expand Down Expand Up @@ -367,9 +359,6 @@ CPPreVote(index) ==
/\ states[index].name = "cp:pre-vote"
/\
\/
/\
\/ states[index].cp_round = MaxCPRound
\/ CPHasOneThirdMainVotesOneInPrvRound(index)
/\ CPHasOneMainVotesOneInPrvRound(index)
/\ SendCPPreVote(index, 1)
\/
Expand Down Expand Up @@ -405,18 +394,32 @@ CPMainVote(index) ==
CPDecide(index) ==
/\ ~IsFaulty(index)
/\ states[index].name = "cp:decide"
/\ CPHasMainVotesQuorum(index)
/\ IF CPHasMainVotesQuorumForOne(index)
THEN /\ SendCPVotesForNextRound(index, 1)
/\
\/
/\ states[index].cp_decided = 1
/\ states' = [states EXCEPT ![index].name = "propose",
![index].round = states[index].round + 1]
ELSE IF CPHasMainVotesQuorumForZero(index)
THEN /\ SendCPVotesForNextRound(index, 0)
/\ states' = [states EXCEPT ![index].name = "prepare"]
ELSE
/\ states' = [states EXCEPT ![index].name = "cp:pre-vote",
![index].cp_round = states[index].cp_round + 1]
/\ log' = log
\/
/\ states[index].cp_decided = 0
/\ states' = [states EXCEPT ![index].name = "prepare"]
\/
/\ states[index].cp_decided = -1
/\ CPHasMainVotesQuorum(index)
/\
IF /\ CPHasMainVotesQuorumForOne(index)
/\ states[index].cp_round /= MaxCPRound - 1
THEN states' = [states EXCEPT ![index].name = "cp:pre-vote",
![index].cp_decided = 1,
![index].cp_round = states[index].cp_round + 1]
ELSE IF \/ CPHasMainVotesQuorumForZero(index)
\/ states[index].cp_round = MaxCPRound - 1
THEN states' = [states EXCEPT ![index].name = "cp:pre-vote",
![index].cp_decided = 0,
![index].cp_round = states[index].cp_round + 1]
ELSE states' = [states EXCEPT ![index].name = "cp:pre-vote",
![index].cp_round = states[index].cp_round + 1]

/\ log' = log


Sync(index) ==
Expand All @@ -434,11 +437,12 @@ Sync(index) ==
Init ==
/\ log = {}
/\ states = [index \in 0..Replicas-1 |-> [
name |-> "new-height",
height |-> 0,
round |-> 0,
timeout |-> FALSE,
cp_round |-> 0]]
name |-> "new-height",
height |-> 0,
round |-> 0,
timeout |-> FALSE,
cp_round |-> 0,
cp_decided |-> -1]]

Next ==
\E index \in 0..Replicas-1:
Expand Down
Loading