From 4e69d42bc2643f8da2f3299630c24a0cd7c3ef2f Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Mon, 23 Oct 2023 17:29:41 +0200 Subject: [PATCH] Do not assert committableIndices of the next state in "replicate", which can cause an error if the log ends on this "replicate". (#5758) Prevents errors such as: ```tla TLC threw an unexpected exception. This was probably caused by an error in the spec or model. See the User Output or TLC Console for clues to what happened. The exception was a java.lang.RuntimeException : Attempted to access index 32 of tuple ... ``` --- tla/consensus/Traceccfraft.tla | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/tla/consensus/Traceccfraft.tla b/tla/consensus/Traceccfraft.tla index 06afdb3ddd12..3a09e5b6555f 100644 --- a/tla/consensus/Traceccfraft.tla +++ b/tla/consensus/Traceccfraft.tla @@ -218,7 +218,13 @@ IsSignCommittableMessages == /\ IsEvent("replicate") /\ logline.msg.globally_committable /\ SignCommittableMessages(logline.msg.state.node_id) - /\ committableIndices[logline.msg.state.node_id]' = Range(logline'.msg.committable_indices) + \* It is tempting to assert the effect of SignCommittableMessages(...node_id) here, i.e., + \* committableIndices'[logline.msg.state.node_id] = Range(logline'.msg.committable_indices). + \* However, this assumes logline', i.e., TraceLog[l'], is less than or equal Len(TraceLog), + \* which is not the case if the logs ends after this "replicate" line. If it does not end, + \* the subsequent send_append_entries will assert the effect of SignCommittableMessages anyway. + \* Also see IsExecuteAppendEntries below. + /\ committableIndices[logline.msg.state.node_id] = Range(logline.msg.committable_indices) IsAdvanceCommitIndex == \* This is enabled *after* a SignCommittableMessages because ACI looks for a @@ -295,6 +301,7 @@ IsExecuteAppendEntries == /\ state[logline.msg.state.node_id] = Follower /\ currentTerm[logline.msg.state.node_id] = logline.msg.state.current_view \* Not asserting committableIndices here because the impl and spec will only be in sync upon the subsequent send_append_entries. + \* Also see IsSignCommittableMessages above. /\ UNCHANGED vars IsRcvRequestVoteResponse ==