Merge branch 'turn_off_lto_when_using_tsan' of https://github.com/ach…

…amayou/CCF into turn_off_lto_when_using_tsan

tests/e2e_batched.py

@@ -17,7 +17,6 @@
 
 
 @reqs.description("Running batch submission of new entries")
-@reqs.supports_methods("/app/batch/submit", "/app/batch/fetch")
 def test(network, args, batch_size=100, write_key_divisor=1, write_size_multiplier=1):
     LOG.info(f"Number of batched entries: {batch_size}")
     primary, _ = network.find_primary()

tests/raft_scenarios/5879_deprecated

@@ -0,0 +1,65 @@
+nodes,0,1
+connect,0,1
+
+# Node 0 starts first, and begins sending messages first
+periodic_one,0,110
+dispatch_all
+
+periodic_all,30
+dispatch_all
+
+state_all
+assert_is_primary,0
+assert_is_backup,1
+
+## ... with the same logs upto index 7.
+replicate,1,txAtIdx1
+replicate,1,txAtIdx2
+replicate,1,txAtIdx3
+replicate,1,txAtIdx4
+replicate,1,txAtIdx5
+replicate,1,txAtIdx6
+emit_signature,1
+periodic_all,30
+dispatch_all
+
+assert_commit_idx,0,7
+assert_commit_idx,1,0
+
+periodic_all,30
+dispatch_all
+assert_state_sync
+
+assert_commit_idx,0,7
+assert_commit_idx,1,7
+
+## At index 8, the leader n2 reconfigures to remove n1.
+replicate_new_configuration,1,0
+
+periodic_all,30
+dispatch_all
+
+state_all
+assert_is_primary,0
+assert_is_backup,1
+## Index 9 is a signature, index 10 some random transaction and index 11 is a signature. 
+emit_signature,1
+assert_commit_idx,0,7
+
+replicate,1,txAt10
+assert_commit_idx,0,7
+
+emit_signature,1
+assert_commit_idx,0,7
+
+
+## When the ACI action taken by n2, it should be able to commit index 11 but instead it will commit index 9.
+periodic_all,30
+dispatch_all
+
+assert_is_primary,0
+assert_is_backup,1
+assert_is_retired,1
+
+assert_commit_idx,0,11
+assert_commit_idx,1,7

tla/consensus/ccfraft.tla

@@ -669,38 +669,47 @@ ChangeConfiguration(i) ==
 AdvanceCommitIndex(i) ==
     /\ state[i] = Leader
     /\ LET
-        \* We want to get the smallest such index forward that is a signature
-        \* This index must be from the current term, 
-        \* as explained by Figure 8 and Section 5.4.2 of https://raft.github.io/raft.pdf
-        \* See find_highest_possible_committable_index in raft.h
-        new_index == SelectInSubSeq(log[i], commitIndex[i]+1, Len(log[i]),
-            LAMBDA e : e.contentType = TypeSignature /\ e.term = currentTerm[i])
-        new_log ==
-            IF new_index > 1 THEN
-               [ j \in 1..new_index |-> log[i][j] ]
-            ELSE
-                  << >>
-        new_config_index == LastConfigurationToIndex(i, new_index)
-        new_configurations == RestrictDomain(configurations[i], LAMBDA c : c >= new_config_index)
+            \* Select those configs that need to have a quorum to agree on this leader.
+            \* Compare https://github.com/microsoft/CCF/blob/75670480c53519fcec1a09d36aefc11b23a597f9/src/consensus/aft/raft.h#L2081
+            HasConsensusWatermark(idx) ==
+                \A config \in {c \in DOMAIN(configurations[i]) : idx >= c } :
+                    \* In all of these configs, we now need a quorum in the servers that have the correct matchIndex
+                    LET config_servers == configurations[i][config]
+                        required_quorum == Quorums[config_servers]
+                        agree_servers == {k \in config_servers : matchIndex[i][k] >= idx}
+                    IN (IF i \in config_servers THEN {i} ELSE {}) \cup agree_servers \in required_quorum
+            \* The function find_highest_possible_committable_index in raft.h returns the largest committable index
+            \* in the current term (Figure 8 and Section 5.4.2 of https://raft.github.io/raft.pdf explains why it has
+            \* to be the *current* term).  Finding the largest index is an (implementation-level) optimization that
+            \* reduces the number of AdvanceCommitIndex calls, but this optimization also shrinks this spec's state-space.
+            \*
+            \* Theoretically, any committable index in the current term works, i.e., highestCommittableIndex could be
+            \* defined non-deterministically as:
+            \*       \E idx \in { j \in (commitIndex[i]+1)..Len(log[i]) : /\ log[i][j].term = currentTerm[i] 
+            \*                                                            /\ log[i][j].contentType = TypeSignature }
+            \*          /\ HasConsensusWatermark(idx)
+            \*          /\ ...
+            \* 
+            \* Max({0} \cup {...}) to default to 0 if no committable index is found.
+            highestCommittableIndex == Max({0} \cup { j \in (commitIndex[i]+1)..Len(log[i]) : 
+                                                                    /\ log[i][j].term = currentTerm[i] 
+                                                                    /\ log[i][j].contentType = TypeSignature
+                                                                    /\ HasConsensusWatermark(j) })
         IN
-        /\  \* Select those configs that need to have a quorum to agree on this leader
-            \A config \in {c \in DOMAIN(configurations[i]) : new_index >= c } :
-                \* In all of these configs, we now need a quorum in the servers that have the correct matchIndex
-                LET config_servers == configurations[i][config]
-                    required_quorum == Quorums[config_servers]
-                    agree_servers == {k \in config_servers : matchIndex[i][k] >= new_index}
-                IN (IF i \in config_servers THEN {i} ELSE {}) \cup agree_servers \in required_quorum
-         \* only advance if necessary (this is basically a sanity check after the Min above)
-        /\ commitIndex[i] < new_index
-        /\ commitIndex' = [commitIndex EXCEPT ![i] = new_index]
+         \* only advance if necessary (this is basically a sanity)
+        /\ commitIndex[i] < highestCommittableIndex
+        /\ commitIndex' = [commitIndex EXCEPT ![i] = highestCommittableIndex]
         /\ committableIndices' = [ committableIndices EXCEPT ![i] = @ \ 0..commitIndex'[i] ]
         \* If commit index surpasses the next configuration, pop configs, and retire as leader if removed
         /\ IF /\ Cardinality(DOMAIN configurations[i]) > 1
-              /\ new_index >= NextConfigurationIndex(i)
+              /\ highestCommittableIndex >= NextConfigurationIndex(i)
            THEN
+              LET new_configurations == RestrictDomain(configurations[i], 
+                                            LAMBDA c : c >= LastConfigurationToIndex(i, highestCommittableIndex))
+              IN
               /\ configurations' = [configurations EXCEPT ![i] = new_configurations]
               \* Retire if i is not in active configuration anymore
-              /\ IF i \notin configurations[i][Min(DOMAIN new_configurations)]
+              /\ IF i \notin configurations[i][Min(DOMAIN configurations'[i])]
                  THEN \E j \in PlausibleSucessorNodes(i) :
                     /\ state' = [state EXCEPT ![i] = RetiredLeader]
                     /\ LET msg == [type          |-> ProposeVoteRequest,