Skip to content

Specialized tla+ for RaftRs#43

Open
wego1236 wants to merge 6 commits into
pingcap:masterfrom
wego1236:master
Open

Specialized tla+ for RaftRs#43
wego1236 wants to merge 6 commits into
pingcap:masterfrom
wego1236:master

Conversation

@wego1236

@wego1236 wego1236 commented Mar 23, 2024

Copy link
Copy Markdown

We've made a formal specification for Raft in paper "In Search of an Understandable Consensus Algorithm" and a certain scale of model checking to verify the correctness of raft-rs(currently still running). There may exist differences between our specification and Raft in paper or in implementation. Please let us know flaws of specification if you have any question.

@Connor1996

Connor1996 commented Mar 26, 2024

Copy link
Copy Markdown
Member

PTAL @overvenus @tonyxuqqi

Connor1996
Connor1996 reviewed Mar 26, 2024
View reviewed changes
Comment thread RaftRs/.gitignore Outdated
@@ -0,0 +1,2 @@
states
*.jar No newline at end of file

@Connor1996 Connor1996 Mar 26, 2024

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please remove .gitignore

@wego1236 wego1236 Mar 27, 2024

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, I'll do now

Comment thread RaftRs/consensus/UdpNetwork.tla Outdated
(***************************************************************************
API NetGetMsg: Get msg from src -> dst FIFO head
* return msg m
真的需要实现吗？？ 讨论

@Connor1996 Connor1996 Mar 26, 2024

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please tidy up the comments

@wego1236 wego1236 Mar 27, 2024

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ok, i'll do now

@wego1236

wego1236 commented May 7, 2024

Copy link
Copy Markdown
Author

Hi, is there anything else I should add, and if so, can you let me know and I'll change it?

Connor1996
Connor1996 reviewed May 7, 2024
View reviewed changes
Comment thread RaftRs/README.md
Comment thread RaftRs/consensus/RaftRs.tla Outdated
Comment thread RaftRs/consensus/RaftRs.tla Outdated
Comment thread RaftRs/consensus/RaftRsUdp.tla
/\ nextIndex \in [ Servers -> [ Servers -> Nat \ {0} ]]
/\ matchIndex \in [ Servers -> [ Servers -> Nat ]]

\* TypeOkCandidateVars ==

@Connor1996 Connor1996 May 7, 2024

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why comment out

@wego1236 wego1236 May 7, 2024

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is an uncleared comment. I'll clear it.

@Connor1996 Connor1996 May 9, 2024

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

seems it's still not cleared @wego1236

Connor1996
Connor1996 reviewed May 7, 2024
View reviewed changes
Comment thread perf.data Outdated
@Connor1996

Connor1996 commented May 7, 2024

Copy link
Copy Markdown
Member

PTAL @BusyJay

@Connor1996

Connor1996 commented May 20, 2024

Copy link
Copy Markdown
Member

@wego1236 friendly ping

@wego1236

wego1236 commented Jun 9, 2024

Copy link
Copy Markdown
Author

I'm sorry I've been on hold for so long because I had something come up a while ago and I've reworked it, can you guys take a look at it again?

@Connor1996

Connor1996 commented Jun 12, 2024

Copy link
Copy Markdown
Member

@wego1236 Will take a look later

@wego1236

wego1236 commented Jun 12, 2024

Copy link
Copy Markdown
Author

If there is a problem, you can tell me and I'll fix it in time.

@wego1236

wego1236 commented Jun 26, 2024

Copy link
Copy Markdown
Author

Hello, I'd like to ask if there's anything I can push forward with

@Connor1996

Connor1996 commented Jun 26, 2024

Copy link
Copy Markdown
Member

/cc @zhangjinpeng1987

@zhangjinpeng87

zhangjinpeng87 commented Jun 26, 2024

Copy link
Copy Markdown

Seems this PR don't contain this change tikv/raft-rs@3cfa667 @wego1236 would you mind to add it?

@wego1236

wego1236 commented Jul 17, 2024

Copy link
Copy Markdown
Author

I'm going to study it and make changes

@wego1236

wego1236 commented Nov 5, 2024

Copy link
Copy Markdown
Author

I'm sorry for taking so long to reply.
In my model, the concern is the correctness of the log storage, for the log apply I don't have to deal with it specifically here, I try to add the operation about the log apply, but such a problem will lead to a more complicated model, probably don't need to modify it specifically.

@Connor1996

Connor1996 commented Nov 12, 2024

Copy link
Copy Markdown
Member

LGTM overall, PTAL @zhangjinpeng87

@wego1236

wego1236 commented Jan 9, 2025

Copy link
Copy Markdown
Author

What else do I need to do? This is related to my graduation.I need to finish writing my graduation thesis and defend it.

Connor1996
Connor1996 approved these changes Jan 15, 2025
View reviewed changes

@Connor1996 Connor1996 left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@wego1236 wego1236 requested a review from Connor1996 March 9, 2025 07:01
@Connor1996

Connor1996 commented Mar 10, 2025

Copy link
Copy Markdown
Member

PTAL @zhangjinpeng87

@FedericoPonzi FedericoPonzi mentioned this pull request Apr 1, 2026
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Connor1996 Connor1996 Awaiting requested review from Connor1996

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@wego1236 @Connor1996 @zhangjinpeng87