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

Fast path #22

Merged
merged 10 commits into from
Dec 18, 2024
Merged

Fast path #22

merged 10 commits into from
Dec 18, 2024

Conversation

lemmy
Copy link
Collaborator

@lemmy lemmy commented Dec 7, 2024 •
edited
Loading

@lemmy lemmy added the enhancement New feature or request label Dec 7, 2024
@lemmy lemmy requested a review from heidihoward December 9, 2024 04:05
heidihoward
heidihoward reviewed Dec 9, 2024
View reviewed changes
pirateship.tla Outdated Show resolved Hide resolved
heidihoward
heidihoward reviewed Dec 9, 2024
View reviewed changes
pirateship.tla Outdated Show resolved Hide resolved
heidihoward
heidihoward reviewed Dec 10, 2024
View reviewed changes
pirateship.tla Outdated Show resolved Hide resolved
heidihoward
heidihoward approved these changes Dec 16, 2024
View reviewed changes
pirateship.tla Outdated Show resolved Hide resolved
pirateship.tla Show resolved Hide resolved
lemmy added a commit that referenced this pull request Dec 16, 2024
@lemmy
Strengthen implication to biimplication.
3061a0e 
#22 (comment)
Signed-off-by: Markus Alexander Kuppe <[email protected]>
lemmy added a commit that referenced this pull request Dec 16, 2024
@lemmy
Add comment for operator HighestUnanimity
22f68e4 
#22 (comment)
Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy lemmy requested a review from heidihoward December 17, 2024 14:16
@heidihoward heidihoward marked this pull request as ready for review December 17, 2024 16:10
@heidihoward
Copy link
Owner

@lemmy Do you know why this changes causes tlc-simulate to go red?

lemmy added a commit that referenced this pull request Dec 17, 2024
@lemmy
Strengthen implication to biimplication.
8578d97 
#22 (comment)
Signed-off-by: Markus Alexander Kuppe <[email protected]>
lemmy added a commit that referenced this pull request Dec 17, 2024
@lemmy
Add comment for operator HighestUnanimity
0d36089 
#22 (comment)
Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy
Copy link
Collaborator Author

lemmy commented Dec 17, 2024 •
edited
Loading

@lemmy Do you know why this changes causes tlc-simulate to go red?

It’s failing because ByzCommitIndex@1 remains 0. Surprisingly, ByzCommitIndex@2 doesn’t persistently remain 0. Will investigate...

  • ByzCommitIndex@2 # 0 because TLCpirateship!TLCInit defines an initial state with byzCommitIndex = [r \in R |-> 2]. ByzCommitIndex@2 also remains 0 if TLCInit is not substituted for Init.
  • git bisect identifies commit aaf24e0 as the source of the regression.

lemmy added 9 commits December 17, 2024 09:57
@lemmy
Record the (largest) quorum that voted for a QC.
b35d24a 
Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy
Fast Path Unanimity
fc9081d 
Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy
Do not include primary's view in unanimity QC search for fast path.
8cf6864 
Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy
Fast Path Fast Path Unanimity Transitively
96f5fbe 
Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy
Heidi's review
67f7443
@lemmy
Heidi's review 2
a680233 
Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy
Heidi's review 3
6a26659 
Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy
Strengthen implication to biimplication.
3aaf753 
#22 (comment)
Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy
Add comment for operator HighestUnanimity
f9013b9 
#22 (comment)
Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy
Let's rename the parameters r and p to something e.g. local and…
0874023 
… `remote` soon.

Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy lemmy merged commit 6282df3 into main Dec 18, 2024
1 of 2 checks passed
lemmy added a commit that referenced this pull request Dec 18, 2024
@lemmy
Strengthen implication to biimplication.
c5518bf 
#22 (comment)
Signed-off-by: Markus Alexander Kuppe <[email protected]>
lemmy added a commit that referenced this pull request Dec 18, 2024
@lemmy
Add comment for operator HighestUnanimity
5c0f292 
#22 (comment)
Signed-off-by: Markus Alexander Kuppe <[email protected]>
@lemmy lemmy deleted the mku-fastpath branch December 18, 2024 00:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@heidihoward heidihoward Awaiting requested review from heidihoward

Assignees
No one assigned
Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@lemmy @heidihoward