From ac5c6c146651148e05b29d43ebf345898e5d4ab7 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 6 Dec 2024 19:09:29 -0800 Subject: [PATCH] WIP: Fast path Signed-off-by: Markus Alexander Kuppe --- pirateship.tla | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/pirateship.tla b/pirateship.tla index 6acc8bb..4276d9d 100644 --- a/pirateship.tla +++ b/pirateship.tla @@ -301,6 +301,10 @@ CheckViewStability(p) == \A q \in Q: prepareQC'[p][q] >= SelectInSeq(log[p], inView) +HighestUnanimity(l, v) == + LET idx == SelectLastInSeq(l, LAMBDA e: e.byzQCVotes = R /\ e.view = v) + IN IF idx = 0 THEN {0} ELSE l[idx].byzQC + \* Primary p receiving votes from replica r \* Compare: src/consensus/steady_state.rs#do_process_vote ReceiveVote(p, r) == @@ -323,9 +327,11 @@ ReceiveVote(p, r) == /\ IF viewStable'[p] THEN /\ crashCommitIndex' = [crashCommitIndex EXCEPT ![p] = MaxQuorum(CQ, log[p], prepareQC'[p], @)] - \* Compare: ssrc/consensus/commit.rs#maybe_byzantine_commit - /\ byzCommitIndex' = [byzCommitIndex EXCEPT ![p] = - HighestByzQC(SubSeq(log[p],1,MaxQuorum(BQ, log[p], prepareQC'[p], 0)))] + \* Compare: src/consensus/commit.rs#maybe_byzantine_commit + /\ LET bci == HighestByzQC(SubSeq(log[p], 1, MaxQuorum(BQ, log[p], prepareQC'[p], 0))) + \* Compare: src/consensus/commit.rs#maybe_byzantine_commit_by_fast_path + bciFastPath == HighestUnanimity(log[p], view[p]) + IN byzCommitIndex' = [byzCommitIndex EXCEPT ![p] = Max(bciFastPath \cup {bci}) ] ELSE UNCHANGED <> /\ UNCHANGED <>