Skip to content

Specialized tla+ for RaftRs#43

Open
wego1236 wants to merge 6 commits intopingcap:masterfrom
wego1236:master
Open

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

Conversation

@wego1236
Copy link
Copy Markdown

@wego1236 wego1236 commented Mar 23, 2024

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
Copy link
Copy Markdown
Member

Connor1996 commented Mar 26, 2024

PTAL @overvenus @tonyxuqqi

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

@Connor1996 Connor1996 Mar 26, 2024

Choose a reason for hiding this comment

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

Please remove .gitignore

Copy link
Copy Markdown
Author

@wego1236 wego1236 Mar 27, 2024

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

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

@Connor1996 Connor1996 Mar 26, 2024

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

Copy link
Copy Markdown
Author

@wego1236 wego1236 Mar 27, 2024

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
Copy link
Copy Markdown
Author

wego1236 commented May 7, 2024

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
RaftRs/consensus/RaftRsUdp.tla
/\ nextIndex \in [ Servers -> [ Servers -> Nat \ {0} ]]
/\ matchIndex \in [ Servers -> [ Servers -> Nat ]]

\* TypeOkCandidateVars ==
Copy link
Copy Markdown
Member

@Connor1996 Connor1996 May 7, 2024

Choose a reason for hiding this comment

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

why comment out

Copy link
Copy Markdown
Author

@wego1236 wego1236 May 7, 2024

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.

Copy link
Copy Markdown
Member

@Connor1996 Connor1996 May 9, 2024

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
@Connor1996
Copy link
Copy Markdown
Member

Connor1996 commented May 7, 2024

PTAL @BusyJay

@Connor1996
Copy link
Copy Markdown
Member

Connor1996 commented May 20, 2024

@wego1236 friendly ping

@wego1236
Copy link
Copy Markdown
Author

wego1236 commented Jun 9, 2024

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
Copy link
Copy Markdown
Member

Connor1996 commented Jun 12, 2024

@wego1236 Will take a look later

@wego1236
Copy link
Copy Markdown
Author

wego1236 commented Jun 12, 2024

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

@wego1236
Copy link
Copy Markdown
Author

wego1236 commented Jun 26, 2024

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

@Connor1996
Copy link
Copy Markdown
Member

Connor1996 commented Jun 26, 2024

/cc @zhangjinpeng1987

@zhangjinpeng87
Copy link
Copy Markdown

zhangjinpeng87 commented Jun 26, 2024

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

@wego1236
Copy link
Copy Markdown
Author

wego1236 commented Jul 17, 2024

I'm going to study it and make changes

@wego1236
Copy link
Copy Markdown
Author

wego1236 commented Nov 5, 2024

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
Copy link
Copy Markdown
Member

Connor1996 commented Nov 12, 2024

LGTM overall, PTAL @zhangjinpeng87

@wego1236
Copy link
Copy Markdown
Author

wego1236 commented Jan 9, 2025

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
Copy link
Copy Markdown
Member

@Connor1996 Connor1996 left a comment

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
Copy link
Copy Markdown
Member

Connor1996 commented Mar 10, 2025

PTAL @zhangjinpeng87

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