Update CheckQuorum condition from quorum in any config to quorum in every active config (#7375)

Co-authored-by: Copilot <[email protected]>
Co-authored-by: Amaury Chamayou <[email protected]>

Author: 3 people

CHANGELOG.md

@@ -13,6 +13,10 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.
 
 - Removed the unused experimental `ccf.host.triggerSubprocess()` JS API
 
+### Fixed
+
+- CheckQuorum now requires a quorum in every configuration (#7375)
+
 ## [7.0.0-dev4]
 
 [7.0.0-dev4]: https://github.com/microsoft/CCF/releases/tag/ccf-7.0.0-dev4

src/consensus/aft/raft.h

@@ -846,38 +846,36 @@ namespace aft
           node.second.last_ack_timeout += elapsed;
         }
 
-        bool has_quorum_of_backups = false;
-        for (auto const& conf : configurations)
-        {
-          size_t backup_ack_timeout_count = 0;
-          for (auto const& node : conf.nodes)
-          {
-            auto search = all_other_nodes.find(node.first);
-            if (search == all_other_nodes.end())
-            {
-              // Ignore ourselves as primary
-              continue;
-            }
-            if (search->second.last_ack_timeout >= election_timeout)
+        bool every_active_config_has_a_quorum = std::all_of(
+          configurations.begin(),
+          configurations.end(),
+          [this](const Configuration& conf) {
+            size_t live_nodes_in_config = 0;
+            for (auto const& node : conf.nodes)
             {
-              RAFT_DEBUG_FMT(
-                "No ack received from {} in last {}",
-                node.first,
-                election_timeout);
-              backup_ack_timeout_count++;
+              auto search = all_other_nodes.find(node.first);
+              if (
+                // if a (non-self) node is in a configuration, then it is in
+                // all_other_nodes. So if a node in a configuration is not found
+                // in all_other_nodes, it must be self, and hence is live
+                search == all_other_nodes.end() ||
+                // Otherwise we use the most recent ack as a failure probe
+                search->second.last_ack_timeout < election_timeout)
+              {
+                ++live_nodes_in_config;
+              }
+              else
+              {
+                RAFT_DEBUG_FMT(
+                  "No ack received from {} in last {}",
+                  node.first,
+                  election_timeout);
+              }
             }
-          }
-
-          if (backup_ack_timeout_count < get_quorum(conf.nodes.size() - 1))
-          {
-            // If primary has quorum of active backups in _any_ configuration,
-            // it should remain primary
-            has_quorum_of_backups = true;
-            break;
-          }
-        }
+            return live_nodes_in_config >= get_quorum(conf.nodes.size());
+          });
 
-        if (!has_quorum_of_backups)
+        if (!every_active_config_has_a_quorum)
         {
           // CheckQuorum: The primary automatically steps down if there are no
           // active configuration in which it has heard back from a majority of

src/consensus/aft/test/driver.cpp

@@ -267,6 +267,15 @@ int main(int argc, char** argv)
         assert(items.size() == 4);
         driver->assert_detail(items[1], items[2], items[3], false, lineno);
         break;
+      case shash("assert_config"):
+        assert(items.size() >= 3);
+        driver->assert_config(
+          items[1], items[2], {std::next(items.begin(), 3), items.end()});
+        break;
+      case shash("assert_absent_config"):
+        assert(items.size() == 3);
+        driver->assert_absent_config(items[1], items[2]);
+        break;
       case shash("replicate_new_configuration"):
         assert(items.size() >= 3);
         items.erase(items.begin());

src/consensus/aft/test/driver.h

@@ -1321,4 +1321,58 @@ class RaftDriver
         std::to_string((int)lineno)));
     }
   }
+
+  void assert_config(
+    const std::string& node_id,
+    const std::string& config_idx_s,
+    const std::vector<std::string>& node_ids)
+  {
+    auto config_idx = std::stol(config_idx_s);
+    auto details = _nodes.at(node_id).raft->get_details();
+    for (const auto& config : details.configs)
+    {
+      if (config.idx == config_idx)
+      {
+        std::set<std::string> expected_nodes(node_ids.begin(), node_ids.end());
+        std::set<std::string> actual_nodes;
+        for (const auto& [id, _] : config.nodes)
+        {
+          actual_nodes.insert(id);
+        }
+        if (expected_nodes != actual_nodes)
+        {
+          auto actual_str =
+            fmt::format("{{{}}}", fmt::join(actual_nodes, ", "));
+          auto expected_str =
+            fmt::format("{{{}}}", fmt::join(expected_nodes, ", "));
+          throw std::runtime_error(fmt::format(
+            "Node {} configuration at idx {} ({}) does not match expected ({})",
+            node_id,
+            config_idx,
+            actual_str,
+            expected_str));
+        }
+        return;
+      }
+    }
+    throw std::runtime_error(fmt::format(
+      "Node {} does not have a configuration at idx {}", node_id, config_idx));
+  }
+
+  void assert_absent_config(
+    const std::string& node_id, const std::string& config_idx_s)
+  {
+    auto config_idx = std::stol(config_idx_s);
+    auto details = _nodes.at(node_id).raft->get_details();
+    for (const auto& config : details.configs)
+    {
+      if (config.idx == config_idx)
+      {
+        throw std::runtime_error(fmt::format(
+          "Node {} has unexpected configuration at idx {}",
+          node_id,
+          config_idx));
+      }
+    }
+  }
 };

tests/raft_scenarios/check_quorum_012_0

@@ -0,0 +1,48 @@
+start_node,0
+emit_signature,2
+swap_nodes,2,in,1,2
+emit_signature,2
+
+dispatch_all
+periodic_all,10
+dispatch_all
+periodic_all,10
+dispatch_all
+
+# All nodes believe that the only configuration is {0,1,2}
+assert_state_sync
+assert_absent_config,0,1
+assert_config,0,3,0,1,2
+
+disconnect_node,0
+swap_nodes,2,out,1,2
+emit_signature,2
+
+# Only node 0 knows about config {0}, as it is partitioned from nodes 1 and 2
+assert_config,0,3,0,1,2
+assert_config,0,5,0
+
+assert_config,1,3,0,1,2
+assert_absent_config,1,5
+assert_config,2,3,0,1,2
+assert_absent_config,2,5
+
+# Node 0 should step down via CheckQuorum
+periodic_one,0,100
+assert_detail,0,leadership_state,Follower
+
+periodic_one,1,100
+assert_detail,1,leadership_state,Candidate
+
+dispatch_all
+periodic_all,10
+dispatch_all
+periodic_all,10
+dispatch_all
+periodic_all,10
+dispatch_all
+periodic_all,10
+dispatch_all
+
+assert_detail,0,leadership_state,Follower
+assert_detail,1,leadership_state,Leader

tests/raft_scenarios/check_quorum_0_012

@@ -0,0 +1,48 @@
+start_node,0
+emit_signature,2
+swap_nodes,2,in,1,2
+emit_signature,2
+
+periodic_one,0,10
+dispatch_all
+dispatch_all
+periodic_one,0,10
+dispatch_all
+
+
+# All nodes have both configs: {0} and {0,1,2}
+assert_commit_idx,0,4
+assert_absent_config,0,1
+assert_config,0,3,0,1,2
+
+assert_commit_idx,1,2
+assert_config,1,1,0
+assert_config,1,3,0,1,2
+
+assert_commit_idx,2,2
+assert_config,2,1,0
+assert_config,2,3,0,1,2
+
+# Node 0 should step down via CheckQuorum
+disconnect_node,0
+periodic_one,0,100
+assert_detail,0,leadership_state,Follower
+
+# Node 1 should try to start an election but fails without a quorum in {0}
+periodic_one,1,100
+assert_detail,1,leadership_state,Candidate
+
+dispatch_all
+periodic_all,10
+dispatch_all
+periodic_all,10
+dispatch_all
+
+assert_detail,1,leadership_state,Candidate
+
+# Fixup the network to allow a leader to be elected and the test to pass
+reconnect_node,0
+periodic_all,100
+dispatch_all
+periodic_all,10
+dispatch_all

tla/consensus/Traceccfraft.tla

@@ -377,12 +377,12 @@ IsRcvRequestVoteResponse ==
 IsBecomeFollower ==
     /\ IsEvent("become_follower")
     /\ UNCHANGED vars \* UNCHANGED implies that it doesn't matter if we prime the previous variables.
+    \* We don't assert committable and last idx here, as the spec and implementation are out of sync until
+    \* IsSendAppendEntriesResponse or IsSendRequestVote (in the candidate path)
     /\ leadershipState[logline.msg.state.node_id] # Leader
-    /\ Range(logline.msg.state.committable_indices) \subseteq CommittableIndices(logline.msg.state.node_id)
     /\ commitIndex[logline.msg.state.node_id] = logline.msg.state.commit_idx
     /\ leadershipState[logline.msg.state.node_id] = ToLeadershipState[logline.msg.state.leadership_state]
     /\ membershipState[logline.msg.state.node_id] \in ToMembershipState[logline.msg.state.membership_state]
-    /\ Len(log[logline.msg.state.node_id]) = logline.msg.state.last_idx
 
 IsCheckQuorum ==
     /\ IsEvent("become_follower")