The efficiency of HandleAppendEntriesRequest in handling conflicts is low

[liang636600]

Hi, @ongardie , I also found that the HandleAppendEntriesRequest uses a remove 1 entry approach when handling conflicts, which is inefficient and generates many unnecessary states during TLC model checking(worse than #16 ), thus reducing the efficiency of the TLC model checking. I will explain this in detail below.

Scenario: As shown in Figure 1, the leader and follower have the same log entry at index 2. The leader intends to replicate the log entry at index 3 to the follower, who currently has K conflicting entries at index 3 and beyond.

Figure 1. Conflicting scenario.

Conflict handling in HandleAppendEntriesRequest: Whenever the follower receives an AERequest, it removes one log entry from the end of its log if there is a conflict. In the scenario depicted in Figure 1, if there are K conflicts, the follower needs the leader to send K + 2 AERequest to complete the log replication at index 3 (with K AERequests used to remove the K conflicting entries and 2 additional AERequests for log replication, as discussed in Issue #16 ). This approach is inefficient, as only one AERequest is actually needed to complete the log replication process at index 3.

raft.tla/raft.tla

Lines 375 to 381 in 5f55322

	\/ \* conflict: remove 1 entry
	/\ m.mentries /= << >>
	/\ Len(log[i]) >= index
	/\ log[i][index].term /= m.mentries[1].term
	/\ LET new == [index2 \in 1..(Len(log[i]) - 1) |->
	log[i][index2]]
	IN log' = [log EXCEPT ![i] = new]

Harmful impact: This inefficient approach to handling conflicts can lead to numerous unnecessary states during TLC model checking, thereby reducing its efficiency, as detailed in Issue #16 . Issue #16 generates only one unnecessary state directly (Node 2), while Nodes 4 and 5 are indirectly produced by Node 2 through the Next action. Even worse, this method can directly generate K + 1 unnecessary states.

Suggested fix: We recommend modifying the approach to conflict handling based on the original Raft paper by delete the existing entry and all that follow it in a single AERequest.

I'm looking forward to your confirmation, and would be happy to help fix the issue if needed.