This is an automated email from the ASF dual-hosted git repository.
tkhurana pushed a commit to branch PHOENIX-7562-feature-new
in repository https://gitbox.apache.org/repos/asf/phoenix.git
The following commit(s) were added to refs/heads/PHOENIX-7562-feature-new by
this push:
new 8328f3a503 PHOENIX-8027 :- Allow consistent failover to be initiated
only from ACTIVE_IN_SYNC (#2640)
8328f3a503 is described below
commit 8328f3a503cdd3fc0ca88dc7b515bb3f0924a3fc
Author: Lokesh Khurana <[email protected]>
AuthorDate: Wed Oct 21 12:44:14 2026 -0700
PHOENIX-8027 :- Allow consistent failover to be initiated only from
ACTIVE_IN_SYNC (#2640)
* PHOENIX-8027 :- Allow consistent failover to be initiated only from
ACTIVE_IN_SYNC
Failover initiated from ACTIVE_NOT_IN_SYNC (store-and-forward) can promote a
peer that has not yet received the forwarded backlog. HAGroupStoreManager
and
PhoenixHAAdminTool now reject initiate-failover unless the group is
ACTIVE_IN_SYNC; the admin tool prints store-and-forward guidance and returns
RET_VALIDATION_ERROR. The ANIS -> ANISTS transition and the ANISTS -> ATS
sync
mapping are kept for compatibility with in-flight groups and mixed versions.
The TLA+ model is updated so AdminStartFailover requires AIS.
Generated-by: Claude Code (Opus 5.5)
* PHOENIX-8027 :- Start the forwarder after the ANIS rejection checks in
HAGroupStoreManagerIT
The strict ACTIVE_NOT_IN_SYNC / DEGRADED_STANDBY assertions after the
rejected
failover raced the forwarder's anti-flap resync. Create the
ReplicationLogGroup
only after those checks so nothing can move the group back to ACTIVE_IN_SYNC
before they run.
Generated-by: Claude Code (Opus 5.5)
---
.../apache/phoenix/jdbc/HAGroupStoreManager.java | 26 ++++-----
.../apache/phoenix/jdbc/PhoenixHAAdminTool.java | 64 +++++++++++++--------
.../apache/phoenix/jdbc/HAGroupStoreManagerIT.java | 30 ++++++++--
.../apache/phoenix/jdbc/PhoenixHAAdminToolIT.java | 66 ++++++++++++++++++++++
src/main/tla/ConsistentFailover/Admin.tla | 46 ++++++---------
.../tla/ConsistentFailover/ConsistentFailover.tla | 25 ++++----
src/main/tla/ConsistentFailover/DEVELOPING.md | 2 +-
src/main/tla/ConsistentFailover/HAGroupStore.tla | 32 ++++++-----
src/main/tla/ConsistentFailover/README.md | 29 ++++++----
src/main/tla/ConsistentFailover/Types.tla | 8 ++-
src/main/tla/ConsistentFailover/Writer.tla | 6 +-
src/main/tla/ConsistentFailover/markdown/Admin.md | 28 ++++-----
.../markdown/ConsistentFailover.md | 2 +-
.../ConsistentFailover/markdown/HAGroupStore.md | 10 ++--
src/main/tla/ConsistentFailover/markdown/Types.md | 8 ++-
src/main/tla/ConsistentFailover/markdown/Writer.md | 2 +-
16 files changed, 244 insertions(+), 140 deletions(-)
diff --git
a/phoenix-core-client/src/main/java/org/apache/phoenix/jdbc/HAGroupStoreManager.java
b/phoenix-core-client/src/main/java/org/apache/phoenix/jdbc/HAGroupStoreManager.java
index 2e33c5b0c8..5f06e53c4c 100644
---
a/phoenix-core-client/src/main/java/org/apache/phoenix/jdbc/HAGroupStoreManager.java
+++
b/phoenix-core-client/src/main/java/org/apache/phoenix/jdbc/HAGroupStoreManager.java
@@ -384,9 +384,9 @@ public class HAGroupStoreManager {
}
/**
- * Initiates failover on the active cluster by transitioning to the
appropriate TO_STANDBY state.
- * Checks current state and transitions to: - ACTIVE_IN_SYNC_TO_STANDBY if
currently
- * ACTIVE_IN_SYNC - ACTIVE_NOT_IN_SYNC_TO_STANDBY if currently
ACTIVE_NOT_IN_SYNC
+ * Initiates failover on the active cluster by transitioning ACTIVE_IN_SYNC
to
+ * ACTIVE_IN_SYNC_TO_STANDBY. Failover is rejected from ACTIVE_NOT_IN_SYNC
(store-and-forward)
+ * because the peer may not have the backlog yet; wait for the group to
return to ACTIVE_IN_SYNC.
* @param haGroupName name of the HA group
* @return the wait time in milliseconds for state transition, if 0 then the
state transition is
* successful.
@@ -413,19 +413,19 @@ public class HAGroupStoreManager {
}
HAGroupStoreRecord.HAGroupState currentState =
currentRecord.getHAGroupState();
- HAGroupStoreRecord.HAGroupState targetState;
-
- // Determine target state based on current state
- if (currentState == HAGroupStoreRecord.HAGroupState.ACTIVE_IN_SYNC) {
- targetState = HAGroupStoreRecord.HAGroupState.ACTIVE_IN_SYNC_TO_STANDBY;
- } else if (currentState ==
HAGroupStoreRecord.HAGroupState.ACTIVE_NOT_IN_SYNC) {
- targetState =
HAGroupStoreRecord.HAGroupState.ACTIVE_NOT_IN_SYNC_TO_STANDBY;
- } else {
+ if (currentState == HAGroupStoreRecord.HAGroupState.ACTIVE_NOT_IN_SYNC) {
throw new InvalidClusterRoleTransitionException("Cannot initiate
failover from state: "
- + currentState + ". Cluster must be in ACTIVE_IN_SYNC or
ACTIVE_NOT_IN_SYNC state.");
+ + currentState + " for HA group: " + haGroupName + ". Cluster must be
in ACTIVE_IN_SYNC "
+ + "state; wait for the store-and-forward backlog to drain to the peer
and retry.");
+ } else if (currentState != HAGroupStoreRecord.HAGroupState.ACTIVE_IN_SYNC)
{
+ throw new InvalidClusterRoleTransitionException(
+ "Cannot initiate failover from state: " + currentState + " for HA
group: " + haGroupName
+ + ". Cluster must be in ACTIVE_IN_SYNC state.");
}
- return haGroupStoreClient.setHAGroupStatusIfNeeded(targetState);
+ // An AIS -> ANIS race before the write is rejected by transition
validation in the client.
+ return haGroupStoreClient
+
.setHAGroupStatusIfNeeded(HAGroupStoreRecord.HAGroupState.ACTIVE_IN_SYNC_TO_STANDBY);
}
/**
diff --git
a/phoenix-core-client/src/main/java/org/apache/phoenix/jdbc/PhoenixHAAdminTool.java
b/phoenix-core-client/src/main/java/org/apache/phoenix/jdbc/PhoenixHAAdminTool.java
index f295117af8..9d6809293f 100644
---
a/phoenix-core-client/src/main/java/org/apache/phoenix/jdbc/PhoenixHAAdminTool.java
+++
b/phoenix-core-client/src/main/java/org/apache/phoenix/jdbc/PhoenixHAAdminTool.java
@@ -53,6 +53,7 @@ import org.apache.hadoop.conf.Configured;
import org.apache.hadoop.hbase.HBaseConfiguration;
import org.apache.hadoop.util.Tool;
import org.apache.hadoop.util.ToolRunner;
+import org.apache.phoenix.exception.InvalidClusterRoleTransitionException;
import org.apache.phoenix.exception.StaleHAGroupStoreRecordVersionException;
import org.apache.phoenix.jdbc.ClusterRoleRecord.ClusterRole;
import org.apache.phoenix.jdbc.HAGroupStoreRecord.HAGroupState;
@@ -589,12 +590,10 @@ public class PhoenixHAAdminTool extends Configured
implements Tool {
* <ol>
* <li>Parse CLI args: haGroupName (required), timeout (optional, default
120s)</li>
* <li>Read current HAGroupStoreRecord from ZooKeeper to validate state</li>
- * <li>Validate current state allows failover (must be ACTIVE_IN_SYNC or
ACTIVE_NOT_IN_SYNC):
+ * <li>Validate current state allows failover (must be ACTIVE_IN_SYNC):
* <ul>
* <li>ACTIVE_IN_SYNC → ACTIVE_IN_SYNC_TO_STANDBY → STANDBY</li>
- * <li>ACTIVE_NOT_IN_SYNC → ACTIVE_NOT_IN_SYNC_TO_STANDBY →
ACTIVE_IN_SYNC_TO_STANDBY →
- * STANDBY</li>
- * <li>Other states: return RET_VALIDATION_ERROR</li>
+ * <li>ACTIVE_NOT_IN_SYNC (store-and-forward) and other states: return
RET_VALIDATION_ERROR</li>
* </ul>
* </li>
* <li>Execute failover via manager.initiateFailoverOnActiveCluster():
@@ -659,20 +658,17 @@ public class PhoenixHAAdminTool extends Configured
implements Tool {
System.out.println(" Current State: " + currentState);
System.out.println(" Cluster Role: " +
currentRecord.getClusterRole());
- // Determine target state based on current state
- HAGroupState targetState;
- HAGroupState finalExpectedState;
- if (currentState == HAGroupState.ACTIVE_IN_SYNC) {
- targetState = HAGroupState.ACTIVE_IN_SYNC_TO_STANDBY;
- finalExpectedState = HAGroupState.STANDBY;
- } else if (currentState == HAGroupState.ACTIVE_NOT_IN_SYNC) {
- targetState = HAGroupState.ACTIVE_NOT_IN_SYNC_TO_STANDBY;
- finalExpectedState = HAGroupState.STANDBY;
- } else {
+ // Failover is only allowed from ACTIVE_IN_SYNC
+ if (currentState != HAGroupState.ACTIVE_IN_SYNC) {
System.err.println("\n✗ Cannot initiate failover from current state:
" + currentState);
- System.err.println(" Cluster must be in ACTIVE_IN_SYNC or
ACTIVE_NOT_IN_SYNC state.");
+ System.err.println(" Cluster must be in ACTIVE_IN_SYNC state.");
+ if (currentState == HAGroupState.ACTIVE_NOT_IN_SYNC) {
+ printStoreAndForwardFailoverGuidance(haGroupName);
+ }
return RET_VALIDATION_ERROR;
}
+ HAGroupState targetState = HAGroupState.ACTIVE_IN_SYNC_TO_STANDBY;
+ HAGroupState finalExpectedState = HAGroupState.STANDBY;
System.out.println("\n[Step 2] Determining target state...");
System.out.println(" Intermediate State: " + targetState);
@@ -681,7 +677,17 @@ public class PhoenixHAAdminTool extends Configured
implements Tool {
// Perform failover initiation
System.out.println("\n[Step 3] Initiating failover on active
cluster...");
HAGroupStoreManager manager = new HAGroupStoreManager(getConf());
- manager.initiateFailoverOnActiveCluster(haGroupName);
+ try {
+ manager.initiateFailoverOnActiveCluster(haGroupName);
+ } catch (InvalidClusterRoleTransitionException e) {
+ // The state changed after the check above (e.g. AIS -> ANIS);
report as validation.
+ System.err.println("\n✗ Cannot initiate failover: " +
e.getMessage());
+ HAGroupStoreRecord latest =
admin.getHAGroupStoreRecordInZooKeeper(haGroupName).getLeft();
+ if (latest != null && latest.getHAGroupState() ==
HAGroupState.ACTIVE_NOT_IN_SYNC) {
+ printStoreAndForwardFailoverGuidance(haGroupName);
+ }
+ return RET_VALIDATION_ERROR;
+ }
System.out.println(" ✓ Failover initiated");
@@ -1247,6 +1253,20 @@ public class PhoenixHAAdminTool extends Configured
implements Tool {
System.err.println(" update -g " + haGroupName + " -s
<ACTIVE_IN_SYNC|STANDBY> -av -F");
}
+ /**
+ * Print operator guidance shown when failover is attempted from
ACTIVE_NOT_IN_SYNC. The peer may
+ * not yet have the store-and-forward backlog, so failing over now could
lose those writes.
+ */
+ private void printStoreAndForwardFailoverGuidance(String haGroupName) {
+ System.err.println(
+ "\n The cluster is in store-and-forward mode; the peer may not have all
writes yet.");
+ System.err.println(" 1. Check the peer is reachable and healthy (run on
each cluster):");
+ System.err.println(" get-cluster-role-record -g " + haGroupName);
+ System.err.println(" 2. Wait for the backlog to drain; the group
returns to ACTIVE_IN_SYNC"
+ + " automatically.");
+ System.err.println(" 3. Retry: initiate-failover -g " + haGroupName);
+ }
+
/**
* Perform the update operation
*/
@@ -1902,16 +1922,14 @@ public class PhoenixHAAdminTool extends Configured
implements Tool {
System.out.println("Usage: phoenix-consistentha-admin-tool
initiate-failover [options]");
System.out.println();
System.out.println("Description:");
- System.out
- .println(" Initiates failover on the active cluster by transitioning to
the appropriate");
- System.out
- .println(" TO_STANDBY state. The cluster must be in ACTIVE_IN_SYNC or
ACTIVE_NOT_IN_SYNC");
- System.out.println(" state to initiate failover.");
+ System.out.println(" Initiates failover on the active cluster by
transitioning to");
+ System.out.println(
+ " ACTIVE_IN_SYNC_TO_STANDBY. The cluster must be in ACTIVE_IN_SYNC
state; failover");
+ System.out.println(
+ " from ACTIVE_NOT_IN_SYNC (store-and-forward) is rejected until the
backlog drains.");
System.out.println();
System.out.println(" State Transitions:");
System.out.println(" - ACTIVE_IN_SYNC -> ACTIVE_IN_SYNC_TO_STANDBY
-> STANDBY");
- System.out.println(" - ACTIVE_NOT_IN_SYNC ->
ACTIVE_NOT_IN_SYNC_TO_STANDBY -> "
- + "ACTIVE_IN_SYNC_TO_STANDBY -> STANDBY");
System.out.println();
System.out.println("Options:");
System.out.println(" -g, --ha-group <name> HA group name (REQUIRED)");
diff --git
a/phoenix-core/src/it/java/org/apache/phoenix/jdbc/HAGroupStoreManagerIT.java
b/phoenix-core/src/it/java/org/apache/phoenix/jdbc/HAGroupStoreManagerIT.java
index af70a3b37e..cb9f790d51 100644
---
a/phoenix-core/src/it/java/org/apache/phoenix/jdbc/HAGroupStoreManagerIT.java
+++
b/phoenix-core/src/it/java/org/apache/phoenix/jdbc/HAGroupStoreManagerIT.java
@@ -695,8 +695,12 @@ public class HAGroupStoreManagerIT extends HABaseIT {
}, HA_STATE_POLL_INTERVAL_MS, HA_STATE_TRANSITION_TIMEOUT_MS);
}
+ /**
+ * Failover from ACTIVE_NOT_IN_SYNC is rejected without changing either
cluster's state; once the
+ * forwarder drains the backlog and the group returns to ACTIVE_IN_SYNC,
failover succeeds.
+ */
@Test(timeout = 240000)
- public void
testE2EFailoverFromActiveNotInSyncWithAutomaticStateTransitions() throws
Exception {
+ public void testE2EFailoverRejectedFromActiveNotInSyncUntilBackInSync()
throws Exception {
String haGroupName = testName.getMethodName();
Configuration cluster1Conf =
CLUSTERS.getHBaseCluster1().getConfiguration();
Configuration cluster2Conf =
CLUSTERS.getHBaseCluster2().getConfiguration();
@@ -731,9 +735,6 @@ public class HAGroupStoreManagerIT extends HABaseIT {
waitForEffectiveHAGroupState(cluster2HAManager, haGroupName,
HAGroupStoreRecord.HAGroupState.STANDBY);
- HRegionServer regionServer =
CLUSTERS.getHBaseCluster1().getHBaseCluster().getRegionServer(0);
- replicationLogGroup = ReplicationLogGroup
- .get(cluster1Conf, regionServer.getServerName(), haGroupName,
cluster1HAManager).get();
replicationLogReplay = ReplicationLogReplay.get(cluster2Conf,
haGroupName);
replicationLogReplay.startReplay();
@@ -743,6 +744,27 @@ public class HAGroupStoreManagerIT extends HABaseIT {
waitForHAGroupState(cluster2HAManager, haGroupName,
HAGroupStoreRecord.HAGroupState.DEGRADED_STANDBY);
+ try {
+ cluster1HAManager.initiateFailoverOnActiveCluster(haGroupName);
+ fail("Failover from ACTIVE_NOT_IN_SYNC should be rejected");
+ } catch (InvalidClusterRoleTransitionException e) {
+ assertTrue(e.getMessage(),
e.getMessage().contains("store-and-forward"));
+ }
+ // No forwarder exists yet, so nothing can move the group back to
ACTIVE_IN_SYNC here.
+ assertEquals(HAGroupStoreRecord.HAGroupState.ACTIVE_NOT_IN_SYNC,
+
cluster1HAManager.getHAGroupStoreRecord(haGroupName).get().getHAGroupState());
+ assertEquals(HAGroupStoreRecord.HAGroupState.DEGRADED_STANDBY,
+
cluster2HAManager.getHAGroupStoreRecord(haGroupName).get().getHAGroupState());
+
+ // Start the forwarder only now; it finds no backlog and promotes the
group back to
+ // ACTIVE_IN_SYNC.
+ HRegionServer regionServer =
CLUSTERS.getHBaseCluster1().getHBaseCluster().getRegionServer(0);
+ replicationLogGroup = ReplicationLogGroup
+ .get(cluster1Conf, regionServer.getServerName(), haGroupName,
cluster1HAManager).get();
+ waitForHAGroupState(cluster1HAManager, haGroupName,
+ HAGroupStoreRecord.HAGroupState.ACTIVE_IN_SYNC);
+ waitForHAGroupState(cluster2HAManager, haGroupName,
HAGroupStoreRecord.HAGroupState.STANDBY);
+
assertEquals(0L,
cluster1HAManager.initiateFailoverOnActiveCluster(haGroupName));
waitForHAGroupState(cluster1HAManager, haGroupName,
HAGroupStoreRecord.HAGroupState.ACTIVE_IN_SYNC_TO_STANDBY);
diff --git
a/phoenix-core/src/it/java/org/apache/phoenix/jdbc/PhoenixHAAdminToolIT.java
b/phoenix-core/src/it/java/org/apache/phoenix/jdbc/PhoenixHAAdminToolIT.java
index 9fb69457ea..8dcb37d6be 100644
--- a/phoenix-core/src/it/java/org/apache/phoenix/jdbc/PhoenixHAAdminToolIT.java
+++ b/phoenix-core/src/it/java/org/apache/phoenix/jdbc/PhoenixHAAdminToolIT.java
@@ -38,6 +38,7 @@ import static
org.apache.phoenix.jdbc.PhoenixHAAdminTool.RET_VALIDATION_ERROR;
import static org.apache.phoenix.util.PhoenixRuntime.JDBC_PROTOCOL_SEPARATOR;
import static org.apache.phoenix.util.PhoenixRuntime.JDBC_PROTOCOL_ZK;
import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertFalse;
import static org.junit.Assert.assertNotNull;
import static org.junit.Assert.assertTrue;
@@ -801,6 +802,71 @@ public class PhoenixHAAdminToolIT extends HABaseIT {
"✓ Timeout test completed successfully: both clusters stuck in
transition states as expected");
}
+ /**
+ * Test that initiate-failover is rejected with a validation error while the
active cluster is in
+ * ACTIVE_NOT_IN_SYNC (store-and-forward), and that neither cluster's state
is changed.
+ */
+ @Test(timeout = 180000)
+ public void testInitiateFailoverRejectedFromActiveNotInSync() throws
Exception {
+ String anisHaGroupName = "testInitiateFailoverFromAnis_" +
System.currentTimeMillis();
+
+ String zkUrl1 = CLUSTERS.getZkUrl1();
+ String zkUrl2 = CLUSTERS.getZkUrl2();
+
+ HAGroupStoreTestUtil.upsertHAGroupRecordInSystemTable(anisHaGroupName,
zkUrl1, zkUrl2,
+ CLUSTERS.getMasterAddress1(), CLUSTERS.getMasterAddress2(),
+ ClusterRoleRecord.ClusterRole.ACTIVE,
ClusterRoleRecord.ClusterRole.STANDBY, null,
+ CLUSTERS.getHdfsUrl1(), CLUSTERS.getHdfsUrl2());
+ HAGroupStoreTestUtil.upsertHAGroupRecordInSystemTable(anisHaGroupName,
zkUrl1, zkUrl2,
+ CLUSTERS.getMasterAddress1(), CLUSTERS.getMasterAddress2(),
+ ClusterRoleRecord.ClusterRole.ACTIVE,
ClusterRoleRecord.ClusterRole.STANDBY, zkUrl2,
+ CLUSTERS.getHdfsUrl1(), CLUSTERS.getHdfsUrl2());
+
+ HAGroupStoreManager cluster1HAManager =
+ new HAGroupStoreManager(CLUSTERS.getHBaseCluster1().getConfiguration());
+ HAGroupStoreManager cluster2HAManager =
+ new HAGroupStoreManager(CLUSTERS.getHBaseCluster2().getConfiguration());
+ cluster1HAManager.getHAGroupStoreRecord(anisHaGroupName);
+ cluster2HAManager.getHAGroupStoreRecord(anisHaGroupName);
+ waitForHAGroupState(cluster1HAManager, anisHaGroupName,
+ HAGroupStoreRecord.HAGroupState.ACTIVE_IN_SYNC, "Cluster1");
+ waitForHAGroupState(cluster2HAManager, anisHaGroupName,
HAGroupStoreRecord.HAGroupState.STANDBY,
+ "Cluster2");
+
+ // Move the active cluster to store-and-forward. No writer runs here, so
it stays there.
+ assertEquals(0L,
cluster1HAManager.setHAGroupStatusToStoreAndForward(anisHaGroupName));
+ waitForHAGroupState(cluster1HAManager, anisHaGroupName,
+ HAGroupStoreRecord.HAGroupState.ACTIVE_NOT_IN_SYNC, "Cluster1");
+ waitForHAGroupState(cluster2HAManager, anisHaGroupName,
+ HAGroupStoreRecord.HAGroupState.DEGRADED_STANDBY, "Cluster2");
+
+ // The rejection guidance is written to stderr.
+ PrintStream capture = new PrintStream(STDOUT_CAPTURE);
+ System.setOut(capture);
+ System.setErr(capture);
+
+ PhoenixHAAdminTool cluster1AdminTool = new PhoenixHAAdminTool();
+ cluster1AdminTool.setConf(CLUSTERS.getHBaseCluster1().getConfiguration());
+ int ret = ToolRunner.run(cluster1AdminTool,
+ new String[] { "initiate-failover", "-g", anisHaGroupName, "-t", "15" });
+
+ assertEquals("initiate-failover from ACTIVE_NOT_IN_SYNC should be
rejected",
+ RET_VALIDATION_ERROR, ret);
+ String output = STDOUT_CAPTURE.toString();
+ assertTrue("Output should say ACTIVE_IN_SYNC is required",
+ output.contains("Cluster must be in ACTIVE_IN_SYNC state"));
+ assertTrue("Output should explain the store-and-forward rejection",
+ output.contains("store-and-forward"));
+ assertFalse("Output should not report a failover being initiated",
+ output.contains("Failover initiated"));
+
+ // Neither cluster moved.
+ assertEquals(HAGroupStoreRecord.HAGroupState.ACTIVE_NOT_IN_SYNC,
+
cluster1HAManager.getHAGroupStoreRecord(anisHaGroupName).get().getHAGroupState());
+ assertEquals(HAGroupStoreRecord.HAGroupState.DEGRADED_STANDBY,
+
cluster2HAManager.getHAGroupStoreRecord(anisHaGroupName).get().getHAGroupState());
+ }
+
/**
* Test that the update command successfully updates HA group configuration.
This test updates
* multiple attributes using auto-increment version.
diff --git a/src/main/tla/ConsistentFailover/Admin.tla
b/src/main/tla/ConsistentFailover/Admin.tla
index 87d9f7fcf8..43fa7362cc 100644
--- a/src/main/tla/ConsistentFailover/Admin.tla
+++ b/src/main/tla/ConsistentFailover/Admin.tla
@@ -34,15 +34,16 @@ EXTENDS SpecState, Types
---------------------------------------------------------------------------
(*
- * Admin initiates failover on the active cluster.
+ * Admin initiates failover on the active cluster: AIS -> ATS.
*
- * Two paths depending on current state:
+ * Failover is only initiated from AIS. ANIS (store-and-forward) is
+ * rejected because the peer may not yet hold the OUT backlog; the
+ * admin must wait for ANIS -> AIS (ANISToAIS) before retrying.
+ * ANISTS is therefore no longer produced by any action; it remains
+ * in Types and ANISTSToATS to mirror the implementation's
+ * transition table.
*
- * AIS path: AIS -> ATS (in-sync, ready to hand off immediately)
- * ANIS path: ANIS -> ANISTS (not-in-sync, forwarder must drain OUT
- * before ANISTS can advance to ATS)
- *
- * AIS path guards:
+ * Guards:
* The OUT directory must be empty and all live RS must be in SYNC
* mode. DEAD RSes are allowed -- an RS can crash while the cluster
* is AIS without changing the HA group state. The implementation
@@ -50,37 +51,26 @@ EXTENDS SpecState, Types
* writing, so the remaining SYNC RSes and empty OUT dir ensure
* safety.
*
- * ANIS path guards:
- * The implementation only validates the current state (ANIS) and
- * peer state. No outDirEmpty or writer-mode guards -- the
- * forwarder will drain OUT after the transition. The ANISTS ->
- * ATS transition (ANISTSToATS in HAGroupStore.tla) guards on
- * outDirEmpty and the anti-flapping gate.
- *
- * Both paths:
* Peer must be in a stable standby state (S or DS) to prevent
* initiating a new failover during the non-atomic window of a
* previous failover (where the peer may still be in ATS).
* Without this guard, the admin could produce an irrecoverable
- * (ATS, ATS) or (ANISTS, ATS) deadlock.
+ * (ATS, ATS) deadlock. This is an operator-side assumption: the
+ * implementation does not read the peer state before writing ATS.
*
- * Post: Cluster c transitions to ATS or ANISTS, both of which
- * map to the ACTIVE_TO_STANDBY role, blocking mutations
+ * Post: Cluster c transitions to ATS, which maps to the
+ * ACTIVE_TO_STANDBY role, blocking mutations
* (isMutationBlocked()=true).
*
- * Source: initiateFailoverOnActiveCluster() checks current
- * state and selects AIS -> ATS or ANIS -> ANISTS.
- * Peer-state guard: getHAGroupStoreRecordFromPeer()
- * (HAGroupStoreClient).
+ * Source: initiateFailoverOnActiveCluster() rejects any state other
+ * than AIS and writes AIS -> ATS.
*)
AdminStartFailover(c) ==
/\ clusterState[Peer(c)] \in {"S", "DS"}
- /\ \/ /\ clusterState[c] = "AIS"
- /\ outDirEmpty[c]
- /\ \A rs \in RS : writerMode[c][rs] \in {"SYNC", "DEAD"}
- /\ clusterState' = [clusterState EXCEPT ![c] = "ATS"]
- \/ /\ clusterState[c] = "ANIS"
- /\ clusterState' = [clusterState EXCEPT ![c] = "ANISTS"]
+ /\ clusterState[c] = "AIS"
+ /\ outDirEmpty[c]
+ /\ \A rs \in RS : writerMode[c][rs] \in {"SYNC", "DEAD"}
+ /\ clusterState' = [clusterState EXCEPT ![c] = "ATS"]
/\ UNCHANGED <<writerVars, replayVars, envVars,
outDirEmpty, antiFlapTimer,
failoverPending, inProgressDirEmpty>>
diff --git a/src/main/tla/ConsistentFailover/ConsistentFailover.tla
b/src/main/tla/ConsistentFailover/ConsistentFailover.tla
index 5300258685..d47ba88509 100644
--- a/src/main/tla/ConsistentFailover/ConsistentFailover.tla
+++ b/src/main/tla/ConsistentFailover/ConsistentFailover.tla
@@ -54,7 +54,7 @@
* | .setHAGroupStatusToSync()
* | ANISTS -> ATS (drain completion)
* AdminStartFailover | initiateFailoverOnActiveCluster()
- * | AIS -> ATS or ANIS -> ANISTS
+ * | AIS -> ATS (rejected from ANIS)
* AdminAbortFailover | setHAGroupStatusToAbortToStandby()
* AdminGoOffline | PhoenixHAAdminTool update --state OFFLINE
* | (gated on UseOfflinePeerDetection)
@@ -268,7 +268,7 @@ Next ==
\* [ZK watcher] Peer-reactive: active detects peer left OFFLINE.
\* (gated on UseOfflinePeerDetection)
\/ haGroupStore!PeerRecoverFromOFFLINE(c)
- \* [Direct ZK write] Admin initiates failover: AIS->ATS or
ANIS->ANISTS.
+ \* [Direct ZK write] Admin initiates failover: AIS->ATS only.
\/ admin!AdminStartFailover(c)
\* [Direct ZK write] Admin aborts failover: STA->AbTS.
\/ admin!AdminAbortFailover(c)
@@ -565,9 +565,9 @@ FailoverCompletion ==
* -> anti-flap timer expires (Tick)
* -> ANIS -> AIS (ANISToAIS)
*
- * The cluster may also leave ANIS via failover (ANIS -> ANISTS),
- * which satisfies the consequent. Under SF on HDFSUp, HDFS
- * cannot be permanently down.
+ * Failover is not initiated from ANIS (AdminStartFailover requires
+ * AIS), so recovery to AIS is the only admin-independent exit.
+ * Under SF on HDFSUp, HDFS cannot be permanently down.
*
* Predicated on ZLA (encoded in Fairness).
*)
@@ -743,7 +743,7 @@ WriterTransitionValid ==
* The implementation checks clusterState = AIS, not per-RS modes.
*
* Source: initiateFailoverOnActiveCluster() (validates
- * current state is AIS or ANIS); the precondition holds
+ * current state is AIS); the precondition holds
* because AIS is only reachable when OUT dir is empty and
* all writers have returned to SYNC. RS crash does not
* change clusterState.
@@ -773,7 +773,8 @@ AntiFlapGate ==
(*
* ANISTS-to-ATS precondition: the ANISTS -> ATS transition
- * (forwarder drain completion during ANIS failover) can only
+ * (forwarder drain completion; legacy path, never enabled because
+ * AdminStartFailover no longer produces ANISTS) can only
* proceed when the OUT directory is empty and the anti-flapping
* gate is open. Cross-checks the ANISTSToATS action's guards,
* analogous to how AIStoATSPrecondition cross-checks
@@ -907,13 +908,11 @@ AISImpliesInSync ==
* degradation actions (WriterToStoreFwd, WriterInitToStoreFwd,
* WriterSyncFwdToStoreFwd, etc.).
*
- * ANISTS: preserves degraded writers from ANIS via
- * AdminStartFailover (writer state unchanged).
+ * ANISTS: would preserve degraded writers from ANIS; no action
+ * produces ANISTS since AdminStartFailover requires AIS.
*
- * ATS: the ANIS failover path enters ATS via ANISTSToATS, which
- * requires outDirEmpty (no STORE_AND_FORWARD writers remain) but
- * does NOT snap SYNC_AND_FWD writers. So ATS may carry
- * SYNC_AND_FWD writers into the abort-resolution path.
+ * ATS: kept in the allowed set because ANISTSToATS (never enabled
+ * while ANISTS is unreachable) does NOT snap SYNC_AND_FWD writers.
*
* AbTAIS: preserves SYNC_AND_FWD writers from ATS via
* PeerReactToAbTS. AutoComplete's AbTAIS -> AIS clause
diff --git a/src/main/tla/ConsistentFailover/DEVELOPING.md
b/src/main/tla/ConsistentFailover/DEVELOPING.md
index a690c1d303..e16fc43914 100644
--- a/src/main/tla/ConsistentFailover/DEVELOPING.md
+++ b/src/main/tla/ConsistentFailover/DEVELOPING.md
@@ -216,7 +216,7 @@ code you are changing:
| `createLocalStateTransitions()` | `HAGroupStore.tla` | `AutoComplete`
(AbTS->S, AbTAIS->AIS, AbTANIS->ANIS) |
| `StoreAndForwardModeImpl.startHAGroupStoreUpdateTask()` | `HAGroupStore.tla`
| `ANISHeartbeat` |
| `HAGroupStoreManager.setHAGroupStatusToSync()` | `HAGroupStore.tla` |
`ANISToAIS`, `ANISTSToATS` |
-| `initiateFailoverOnActiveCluster()` | `Admin.tla` | `AdminStartFailover`
(AIS->ATS or ANIS->ANISTS) |
+| `initiateFailoverOnActiveCluster()` | `Admin.tla` | `AdminStartFailover`
(AIS->ATS; rejected from ANIS) |
| `setHAGroupStatusToAbortToStandby()` | `Admin.tla` | `AdminAbortFailover`
(STA->AbTS) |
| `SyncModeImpl.onFailure()` | `Writer.tla` | `WriterToStoreFwd`,
`WriterToStoreFwdFail` |
| `SyncAndForwardModeImpl.onFailure()` | `Writer.tla` |
`WriterSyncFwdToStoreFwd`, `WriterSyncFwdToStoreFwdFail` |
diff --git a/src/main/tla/ConsistentFailover/HAGroupStore.tla
b/src/main/tla/ConsistentFailover/HAGroupStore.tla
index a2e4311637..0b7734cba2 100644
--- a/src/main/tla/ConsistentFailover/HAGroupStore.tla
+++ b/src/main/tla/ConsistentFailover/HAGroupStore.tla
@@ -115,9 +115,8 @@ ResetToStandbyEntry(c) ==
*
* When the standby detects its peer has entered ATS, it begins the
* failover process by transitioning to STA (STANDBY_TO_ACTIVE).
- * This fires from either S or DS -- the DS case supports the ANIS
- * failover path where the standby is in DEGRADED_STANDBY when
- * failover proceeds.
+ * This fires from either S or DS -- the DS case covers a standby
+ * that has not yet observed the active's return from ANIS to AIS.
*
* ZK watcher dependency: Delivered via peerPathChildrenCache.
* Guarded on zkPeerConnected[c] and zkPeerSessionAlive[c].
@@ -240,13 +239,14 @@ PeerReactToAbTS(c) ==
* ANISToAIS. This models the ACTIVE_IN_SYNC ZK event firing
* ReplicationLogDiscoveryForwarder.init(), which snaps SYNC_AND_FWD
* writers atomically with the cluster-state change. SYNC_AND_FWD
- * writers can be carried into AbTAIS via the ANIS -> ANISTS -> ATS
- * -> AbTAIS path (writer state preserved across ANISTSToATS,
- * PeerReactToAbTS); without the snap, AbTAIS -> AIS would expose
+ * writers could only reach AbTAIS via the legacy ANIS -> ANISTS ->
+ * ATS -> AbTAIS path (writer state preserved across ANISTSToATS,
+ * PeerReactToAbTS), which AdminStartFailover no longer produces;
+ * the snap is kept so AbTAIS -> AIS can never expose
* (AIS, SYNC_AND_FWD) and violate AISImpliesInSync. STORE_AND_FWD
- * writers are unreachable in AbTAIS post-Option-B because
- * ANISTSToATS requires outDirEmpty, which is only TRUE when no
- * STORE_AND_FWD writer remains.
+ * writers are unreachable in AbTAIS because ANISTSToATS requires
+ * outDirEmpty, which is only TRUE when no STORE_AND_FWD writer
+ * remains.
*
* Source: createLocalStateTransitions() in HAGroupStoreManager.java
* AbTS -> S -- atomically sets replayState =
@@ -306,10 +306,10 @@ AutoComplete(c) ==
* directory is cleared (outDirEmpty = TRUE). DEAD writers are
* preserved: a crashed RS (JVM dead) cannot process the state
* change notification; the process supervisor restart (RSRestart)
- * handles DEAD -> INIT independently. This is critical for the
- * ANIS failover path where SYNC_AND_FWD or STORE_AND_FWD writers
- * may persist through ANISTS -> ATS (ANISTSToATS does not snap
- * writer modes).
+ * handles DEAD -> INIT independently. On the legacy ANIS failover
+ * path (not produced by AdminStartFailover), SYNC_AND_FWD writers
+ * could persist through ANISTS -> ATS (ANISTSToATS does not snap
+ * writer modes); the reset covers that case too.
*
* ZK watcher dependency: Delivered via peerPathChildrenCache.
* Guarded on zkPeerConnected[c] and zkPeerSessionAlive[c].
@@ -419,12 +419,16 @@ ANISToAIS(c) ==
(*
* Drain completion: ANISTS -> ATS.
*
+ * ANISTS is not produced by AdminStartFailover (failover requires
+ * AIS), so this action is never enabled in the current model. It is kept
+ * to mirror setHAGroupStatusToSync()'s ANISTS -> ATS mapping.
+ *
* When the forwarder has drained the OUT directory and the anti-
* flapping gate has opened, the cluster advances from ANISTS
* (ACTIVE_NOT_IN_SYNC_TO_STANDBY) to ATS
* (ACTIVE_IN_SYNC_TO_STANDBY), joining the normal AIS failover
* path. The standby reacts to ATS (not ANISTS), so this
- * transition is the bridge that lets the ANIS failover path
+ * transition is the bridge that lets the legacy ANIS failover path
* converge with the AIS failover path.
*
* Writer modes are NOT snapped here. In the implementation,
diff --git a/src/main/tla/ConsistentFailover/README.md
b/src/main/tla/ConsistentFailover/README.md
index 7bebe2dbce..db14a34d29 100644
--- a/src/main/tla/ConsistentFailover/README.md
+++ b/src/main/tla/ConsistentFailover/README.md
@@ -24,7 +24,7 @@ Literate programming versions of all specification files are
available in the [`
| Literate Version | Source | Description |
|-----------------|--------|-------------|
| [`HAGroupStore.md`](markdown/HAGroupStore.md) |
[`HAGroupStore.tla`](HAGroupStore.tla) | Peer-reactive transitions,
auto-completion, S&F heartbeat, ANIS recovery, ANISTS drain, retry exhaustion |
-| [`Admin.md`](markdown/Admin.md) | [`Admin.tla`](Admin.tla) |
Operator-initiated failover (AIS->ATS, ANIS->ANISTS) and abort (STA->AbTS) |
+| [`Admin.md`](markdown/Admin.md) | [`Admin.tla`](Admin.tla) |
Operator-initiated failover (AIS->ATS only) and abort (STA->AbTS) |
| [`Writer.md`](markdown/Writer.md) | [`Writer.tla`](Writer.tla) | Per-RS
writer mode state machine: startup, degradation (CAS success/failure),
recovery, drain |
| [`Reader.md`](markdown/Reader.md) | [`Reader.tla`](Reader.tla) | Standby
replay state machine: advance, rewind, in-progress directory, failover trigger |
@@ -108,7 +108,7 @@ Each cluster's lifecycle: `ACTIVE_IN_SYNC`,
`ACTIVE_NOT_IN_SYNC`, `ACTIVE_IN_SYN
`NOT_INITIALIZED`, `SYNC` (fully in sync), `DEGRADED` (active peer in `ANIS`;
`lastRoundInSync` frozen), `SYNCED_RECOVERY` (active returned to `AIS`; replay
rewinds to `lastRoundInSync`).
**Combined Product State.**
-The (ActiveClusterState, StandbyClusterState) pair progresses through a
well-defined sequence during failover. AIS path: `(AIS,S)` -> `(ATS,S)` ->
`(ATS,STA)` -> `(ATS,AIS)` -> `(S,AIS)`. ANIS path: `(ANIS,DS)` ->
`(ANISTS,DS)` -> `(ATS,DS)` -> `(ATS,STA)` -> `(ATS,AIS)` -> `(S,AIS)`.
+The (ActiveClusterState, StandbyClusterState) pair progresses through a
well-defined sequence during failover. `(AIS,S)` -> `(ATS,S)` -> `(ATS,STA)` ->
`(ATS,AIS)` -> `(S,AIS)`. Failover is not initiated from `ANIS`; the active
must first return to `AIS`.
**Anti-Flapping Timer.**
A countdown timer (Lamport CHARME 2005) gates the `ANIS` -> `AIS` transition:
the OUT directory must remain empty and all RS must be in SYNC for a
configurable number of ticks before the cluster may return to `ACTIVE_IN_SYNC`.
@@ -124,9 +124,9 @@ The final failover step is two independent ZK writes. The
new active writes `ACT
### Failover Sequence
-1. **Initiation.** Admin transitions the active cluster from `AIS` to `ATS`
(AIS failover path) or from `ANIS` to `ANISTS` (ANIS failover path). The
`ACTIVE_TO_STANDBY` role blocks all mutations. On the ANIS path, the forwarder
must drain the OUT directory and the anti-flapping gate must open before
`ANISTS` advances to `ATS`.
+1. **Initiation.** Admin transitions the active cluster from `AIS` to `ATS`.
The `ACTIVE_TO_STANDBY` role blocks all mutations. Failover is rejected from
`ANIS` (store-and-forward) because the peer may not yet hold the OUT backlog.
-2. **Standby detection.** The standby's `FailoverManagementListener` detects
the peer's ATS via a ZK watcher and reactively transitions the standby from `S`
(or `DS` on the ANIS path) to `STA`. This sets `failoverPending = true`.
+2. **Standby detection.** The standby's `FailoverManagementListener` detects
the peer's ATS via a ZK watcher and reactively transitions the standby from `S`
(or `DS`, if it has not yet observed the active's return to `AIS`) to `STA`.
This sets `failoverPending = true`.
3. **Log replay.** The standby replays all outstanding replication logs. The
failover trigger requires: `failoverPending`, in-progress directory empty, and
no new files in the time window (`lastRoundProcessed >= lastRoundInSync`).
@@ -172,7 +172,7 @@ Liveness properties guarantee progress. Transient states
eventually resolve to s
| Property | Clauses | Description |
|----------|---------|-------------|
| `FailoverCompletion` | 15 | Standby-side and abort transient states (`STA`,
`AbTAIS`, `AbTANIS`, `AbTS`) eventually resolve to a stable state (`AIS`,
`ANIS`, `S`). ATS/ANISTS excluded: resolution depends on peer state and ZK
connectivity at the right moment, with no fairness on admin actions or ZK
disconnect. |
-| `DegradationRecovery` | 25 | ANIS with available peer HDFS eventually
progresses out of ANIS via the writer recovery chain: `S&F` -> `S&FWD` ->
`SYNC`, anti-flap timer expires, `ANIS` -> `AIS`. May also leave ANIS via
failover (`ANIS` -> `ANISTS`). |
+| `DegradationRecovery` | 25 | ANIS with available peer HDFS eventually
progresses out of ANIS via the writer recovery chain: `S&F` -> `S&FWD` ->
`SYNC`, anti-flap timer expires, `ANIS` -> `AIS`. |
| `AbortCompletion` | 5 | Every abort state (`AbTS`, `AbTAIS`, `AbTANIS`)
eventually auto-completes to a stable state (`AIS`, `ANIS`, `S`). Deterministic
under WF on `AutoComplete`. |
## Module Architecture
@@ -204,7 +204,7 @@ All sub-modules extend `SpecState.tla` and `Types.tla` for
shared variables and
| `Types.tla` | Pure definitions: 14 HA group states, allowed transitions,
cluster roles, writer modes, replay states, liveness state sets, writer/replay
transition tables, anti-flapping timer helpers. No variables. |
| `ConsistentFailover.tla` | Root orchestrator. Defines
Init/Next/SafetySpec/Spec, instances sub-modules, defines all invariants and
action constraints. |
| `HAGroupStore.tla` | 11 action schemas. Peer-reactive transitions
(`PeerReactToATS`, `PeerReactToANIS`, `PeerReactToAbTS`, `PeerReactToAIS`),
local auto-completion (`AutoComplete`), STORE_AND_FORWARD heartbeat
(`ANISHeartbeat`), ANIS recovery (`ANISToAIS`), ANISTS drain completion
(`ANISTSToATS`), retry exhaustion (`ReactiveTransitionFail`), peer OFFLINE
detection (`PeerReactToOFFLINE`, `PeerRecoverFromOFFLINE`). ATS->S transitions
include writer lifecycle reset (live writers reset to [...]
-| `Admin.tla` | `AdminStartFailover` (AIS->ATS or ANIS->ANISTS with peer-state
guard), `AdminAbortFailover` (STA->AbTS, clears failoverPending),
`AdminGoOffline` (S/DS->OFFLINE, gated on `UseOfflinePeerDetection`), and
`AdminForceRecover` (OFFLINE->S, gated on `UseOfflinePeerDetection`). |
+| `Admin.tla` | `AdminStartFailover` (AIS->ATS with peer-state guard; rejected
from ANIS), `AdminAbortFailover` (STA->AbTS, clears failoverPending),
`AdminGoOffline` (S/DS->OFFLINE, gated on `UseOfflinePeerDetection`), and
`AdminForceRecover` (OFFLINE->S, gated on `UseOfflinePeerDetection`). |
| `Writer.tla` | Per-RS writer mode transitions: startup (`WriterInit`,
`WriterInitToStoreFwd`, `WriterInitToStoreFwdFail`), degradation
(`WriterToStoreFwd`, `WriterToStoreFwdFail`, `WriterSyncFwdToStoreFwd`,
`WriterSyncFwdToStoreFwdFail`), recovery (`WriterSyncToSyncFwd`,
`WriterStoreFwdToSyncFwd`), drain complete (`WriterSyncFwdToSync`). ZK-writing
actions guarded on `zkLocalConnected`. |
| `Reader.tla` | Replay advance (SYNC and DEGRADED), rewind, in-progress
directory dynamics, failover trigger (`TriggerFailover` guarded on
`zkLocalConnected`). Listener effects (degradedListener, recoveryListener) are
folded into HAGroupStore S/DS-entry actions. |
| `HDFS.tla` | `HDFSDown` and `HDFSUp` -- environment actions for NameNode
crash/recovery. |
@@ -341,19 +341,24 @@ java -XX:+UseParallelGC \
| Metric | Value |
|--------|-------|
| Configuration | 2 clusters, 2 RS per cluster, WaitTimeForSync=2 |
-| Workers | 16 |
-| States generated | 1,107,584,929 |
-| Distinct states | 70,543,872 |
-| Depth | 54 |
-| Duration | 10 min 14 sec |
-| Date | 2026-05-22 |
+| Workers | 12 |
+| States generated | 741,025,585 |
+| Distinct states | 46,422,720 |
+| Depth | 55 |
+| Duration | 8 min 42 sec |
+| Date | 2026-10-20 |
| Result | Success |
All 6 state invariants and 9 action constraints verified. No violations.
+`AdminStartFailover` requires AIS, so ANISTS is unreachable and the legacy
+ANIS -> ANISTS -> ATS path kept in the implementation is not exercised;
+`ANISTStoATSPrecondition` holds vacuously.
### Liveness (Per-Property Simulation)
All runs: 2 clusters, 2 RS per cluster, WaitTimeForSync=2, 16 workers, depth
10000, 1 hr.
+These runs predate restricting `AdminStartFailover` to AIS. They remain valid
+because that change only removes behaviors and admin actions carry no fairness.
| Property | Config | States Checked | Traces | Seed | Date | Result |
|----------|--------|----------------|--------|------|------|--------|
diff --git a/src/main/tla/ConsistentFailover/Types.tla
b/src/main/tla/ConsistentFailover/Types.tla
index a3a48d4321..3eed346e3d 100644
--- a/src/main/tla/ConsistentFailover/Types.tla
+++ b/src/main/tla/ConsistentFailover/Types.tla
@@ -227,7 +227,9 @@ ReplayStateSet == {"NOT_INITIALIZED", "SYNC", "DEGRADED",
"SYNCED_RECOVERY"}
AllowedTransitions ==
{
\* ANIS can stay in ANIS (heartbeat), return to AIS (recovery),
- \* begin failover (ANISTS), or detect offline peer (ANISWOP).
+ \* or detect offline peer (ANISWOP). ANIS -> ANISTS (legacy
+ \* failover) mirrors HAGroupStoreRecord.java but is not
+ \* produced by AdminStartFailover, which requires AIS.
<<"ANIS", "ANIS">>,
<<"ANIS", "AIS">>,
<<"ANIS", "ANISTS">>,
@@ -256,8 +258,8 @@ AllowedTransitions ==
<<"STA", "AIS">>,
\* DS can recover to S, begin failover (STA), or go offline
\* (OFFLINE) via admin --force.
- \* DS -> STA supports the ANIS failover path where the
- \* standby is in DEGRADED_STANDBY when failover proceeds.
+ \* DS -> STA covers a standby that has not yet observed the
+ \* active's ANIS -> AIS recovery when the peer enters ATS.
\* Source:; OFFLINE entry via PhoenixHAAdminTool
\* update --force (bypasses isTransitionAllowed)
<<"DS", "S">>,
diff --git a/src/main/tla/ConsistentFailover/Writer.tla
b/src/main/tla/ConsistentFailover/Writer.tla
index 44dd25f5e3..b8de792003 100644
--- a/src/main/tla/ConsistentFailover/Writer.tla
+++ b/src/main/tla/ConsistentFailover/Writer.tla
@@ -145,9 +145,9 @@ WriterInitToStoreFwd(c, rs) ==
* learn that the cluster has entered ANIS and transition to
* SYNC_AND_FWD. This event fires once when the cluster enters ANIS.
* ANISTS does not produce a new ACTIVE_NOT_IN_SYNC event -- it is a
- * different ZK state change (ACTIVE_NOT_IN_SYNC_TO_STANDBY). A SYNC
- * writer that has not yet received the event when ANIS -> ANISTS fires
- * will remain in SYNC.
+ * different ZK state change (ACTIVE_NOT_IN_SYNC_TO_STANDBY). On the
+ * legacy ANIS -> ANISTS path (not produced by AdminStartFailover), a
+ * SYNC writer that has not yet received the event remains in SYNC.
* No ZK write -- mode transition driven by forwarder event.
*
* Source: ReplicationLogDiscoveryForwarder.init()
diff --git a/src/main/tla/ConsistentFailover/markdown/Admin.md
b/src/main/tla/ConsistentFailover/markdown/Admin.md
index 095f8c743c..016eb975bd 100644
--- a/src/main/tla/ConsistentFailover/markdown/Admin.md
+++ b/src/main/tla/ConsistentFailover/markdown/Admin.md
@@ -27,35 +27,29 @@ EXTENDS SpecState, Types
## AdminStartFailover -- Initiate Failover
-The admin initiates failover on the active cluster. Two paths depending on
current state:
+The admin initiates failover on the active cluster: AIS -> ATS. Failover is
only initiated from AIS. ANIS (store-and-forward) is rejected because the peer
may not yet hold the OUT backlog; the admin must wait for ANIS -> AIS
(`ANISToAIS` in [HAGroupStore.md](HAGroupStore.md)) before retrying. ANISTS is
therefore no longer produced by any action; it remains in [Types.md](Types.md)
and `ANISTSToATS` to mirror the implementation's transition table.
-### AIS Path: AIS -> ATS
+### Guards
-The cluster is fully in sync. The OUT directory must be empty and all live RS
must be in SYNC mode. DEAD RSes are allowed -- an RS can crash while the
cluster is AIS without changing the HA group state. The implementation checks
`clusterState = AIS`, not per-RS modes; a DEAD RS is not writing, so the
remaining SYNC RSes and empty OUT dir ensure safety.
+The OUT directory must be empty and all live RS must be in SYNC mode. DEAD
RSes are allowed -- an RS can crash while the cluster is AIS without changing
the HA group state. The implementation checks `clusterState = AIS`, not per-RS
modes; a DEAD RS is not writing, so the remaining SYNC RSes and empty OUT dir
ensure safety.
-### ANIS Path: ANIS -> ANISTS
+### Peer-State Guard
-The cluster is not in sync (at least one RS is in STORE_AND_FWD). The
implementation only validates the current state (ANIS) and peer state -- no
`outDirEmpty` or writer-mode guards are needed because the forwarder will drain
OUT after the transition. The ANISTS -> ATS transition (`ANISTSToATS` in
[HAGroupStore.md](HAGroupStore.md)) guards on `outDirEmpty` and the
anti-flapping gate.
-
-### Peer-State Guard (Both Paths)
-
-The peer must be in a stable standby state (S or DS) to prevent initiating a
new failover during the non-atomic window of a previous failover (where the
peer may still be in ATS). Without this guard, the admin could produce an
irrecoverable `(ATS, ATS)` or `(ANISTS, ATS)` deadlock where both clusters are
transitioning to standby with mutations blocked on both sides.
+The peer must be in a stable standby state (S or DS) to prevent initiating a
new failover during the non-atomic window of a previous failover (where the
peer may still be in ATS). Without this guard, the admin could produce an
irrecoverable `(ATS, ATS)` deadlock where both clusters are transitioning to
standby with mutations blocked on both sides. This is an operator-side
assumption: the implementation does not read the peer state before writing ATS.
### Post-Condition
-Cluster `c` transitions to ATS or ANISTS, both of which map to the
ACTIVE_TO_STANDBY role, blocking mutations (`isMutationBlocked() = true`).
+Cluster `c` transitions to ATS, which maps to the ACTIVE_TO_STANDBY role,
blocking mutations (`isMutationBlocked() = true`).
-Source: `initiateFailoverOnActiveCluster()` checks current state and selects
AIS -> ATS or ANIS -> ANISTS. Peer-state guard:
`getHAGroupStoreRecordFromPeer()` (`HAGroupStoreClient`).
+Source: `initiateFailoverOnActiveCluster()` rejects any state other than AIS
and writes AIS -> ATS.
```tla
AdminStartFailover(c) ==
/\ clusterState[Peer(c)] \in {"S", "DS"}
- /\ \/ /\ clusterState[c] = "AIS"
- /\ outDirEmpty[c]
- /\ \A rs \in RS : writerMode[c][rs] \in {"SYNC", "DEAD"}
- /\ clusterState' = [clusterState EXCEPT ![c] = "ATS"]
- \/ /\ clusterState[c] = "ANIS"
- /\ clusterState' = [clusterState EXCEPT ![c] = "ANISTS"]
+ /\ clusterState[c] = "AIS"
+ /\ outDirEmpty[c]
+ /\ \A rs \in RS : writerMode[c][rs] \in {"SYNC", "DEAD"}
+ /\ clusterState' = [clusterState EXCEPT ![c] = "ATS"]
/\ UNCHANGED <<writerMode, outDirEmpty, hdfsAvailable, antiFlapTimer,
replayState, lastRoundInSync, lastRoundProcessed,
failoverPending, inProgressDirEmpty,
diff --git a/src/main/tla/ConsistentFailover/markdown/ConsistentFailover.md
b/src/main/tla/ConsistentFailover/markdown/ConsistentFailover.md
index 994455587d..2d86059364 100644
--- a/src/main/tla/ConsistentFailover/markdown/ConsistentFailover.md
+++ b/src/main/tla/ConsistentFailover/markdown/ConsistentFailover.md
@@ -470,7 +470,7 @@ DegradationRecovery ==
~> clusterState[c] \in NotANISClusterStates
```
-ANIS with available peer HDFS eventually progresses out of ANIS. The recovery
chain is: S&F -> S&FWD (`WriterStoreFwdToSyncFwd`) -> SYNC
(`WriterSyncFwdToSync`, sets `outDirEmpty`) -> anti-flap timer expires (`Tick`)
-> ANIS -> AIS (`ANISToAIS`). The cluster may also leave ANIS via failover
(ANIS -> ANISTS), which satisfies the consequent.
+ANIS with available peer HDFS eventually progresses out of ANIS. The recovery
chain is: S&F -> S&FWD (`WriterStoreFwdToSyncFwd`) -> SYNC
(`WriterSyncFwdToSync`, sets `outDirEmpty`) -> anti-flap timer expires (`Tick`)
-> ANIS -> AIS (`ANISToAIS`). Failover is not initiated from ANIS
(`AdminStartFailover` requires AIS), so recovery to AIS is the only
admin-independent exit.
### AbortCompletion
diff --git a/src/main/tla/ConsistentFailover/markdown/HAGroupStore.md
b/src/main/tla/ConsistentFailover/markdown/HAGroupStore.md
index 2a43cdf34d..c5c07427f9 100644
--- a/src/main/tla/ConsistentFailover/markdown/HAGroupStore.md
+++ b/src/main/tla/ConsistentFailover/markdown/HAGroupStore.md
@@ -115,7 +115,7 @@ EXTENDS SpecState, Types
## PeerReactToATS -- Standby Detects Peer ATS
-When the standby detects its peer has entered ATS (ACTIVE_IN_SYNC_TO_STANDBY),
it begins the failover process by transitioning to STA (STANDBY_TO_ACTIVE).
This fires from either S or DS -- the DS case supports the ANIS failover path
where the standby is in DEGRADED_STANDBY when failover proceeds.
+When the standby detects its peer has entered ATS (ACTIVE_IN_SYNC_TO_STANDBY),
it begins the failover process by transitioning to STA (STANDBY_TO_ACTIVE).
This fires from either S or DS -- the DS case covers a standby that has not yet
observed the active's return from ANIS to AIS.
**ZK watcher dependency:** Delivered via `peerPathChildrenCache`. Guarded on
`zkPeerConnected[c]` and `zkPeerSessionAlive[c]`. If the peer ZK session
expires or the notification is lost, the standby never learns of the failover.
The active cluster remains in ATS with mutations blocked indefinitely. There is
no polling fallback.
@@ -203,7 +203,7 @@ These transitions fire automatically once the cluster
enters the corresponding a
**AbTAIS -> AIS:** Unconditional cluster-state change -- always completes to
AIS, matching `createLocalStateTransitions()` in `HAGroupStoreManager`. The
implementation relies on a temporal invariant: in mutation-blocked or transient
roles (ATS, ANISTS, AbTAIS, AbTANIS) no client write reaches a writer, so
writers cannot degrade in those states. That invariant is encoded statically in
this spec by the tightened cluster-state guards on the writer-degradation
actions in `Writer.tla` (`Write [...]
-The action atomically snaps any remaining `SYNC_AND_FWD` writers to `SYNC`,
mirroring `ANISToAIS`. This models the ACTIVE_IN_SYNC ZK event firing
`ReplicationLogDiscoveryForwarder.init()`, which transitions `SYNC_AND_FWD`
writers atomically with the cluster-state change. `SYNC_AND_FWD` writers can be
carried into AbTAIS via the ANIS -> ANISTS -> ATS -> AbTAIS path (writer state
preserved across `ANISTSToATS` and `PeerReactToAbTS`); without the snap, AbTAIS
-> AIS would expose `(AIS, SYNC [...]
+The action atomically snaps any remaining `SYNC_AND_FWD` writers to `SYNC`,
mirroring `ANISToAIS`. This models the ACTIVE_IN_SYNC ZK event firing
`ReplicationLogDiscoveryForwarder.init()`, which transitions `SYNC_AND_FWD`
writers atomically with the cluster-state change. `SYNC_AND_FWD` writers could
only reach AbTAIS via the legacy ANIS -> ANISTS -> ATS -> AbTAIS path (writer
state preserved across `ANISTSToATS` and `PeerReactToAbTS`), which
`AdminStartFailover` no longer produces; the s [...]
**AbTANIS -> ANIS:** Returns to ANIS. Resets the anti-flapping timer to
`StartAntiFlapWait`, keeping the gate closed so the cluster must wait before
attempting ANIS -> AIS recovery. Source: `createLocalStateTransitions()`.
@@ -243,7 +243,7 @@ Reactive transitions triggered by the peer entering AIS
(ACTIVE_IN_SYNC):
1. **Local ATS -> S:** Old active completes failover to standby when the peer
(the new active) enters AIS. Atomically sets `replayState = SYNCED_RECOVERY`
(recoveryListener fold). This is the critical transition that resolves the
non-atomic failover window.
2. **Local DS -> S:** Standby recovers from degraded when peer returns to AIS.
Atomically sets `replayState = SYNCED_RECOVERY` (recoveryListener fold).
-**Writer lifecycle reset (ATS -> S):** Same as `PeerReactToANIS` ATS -> S.
Live writer modes reset to INIT, OUT directory cleared. DEAD writers preserved
for `RSRestart`. This is critical for the ANIS failover path where SYNC_AND_FWD
or STORE_AND_FWD writers may persist through ANISTS -> ATS (`ANISTSToATS` does
not snap writer modes).
+**Writer lifecycle reset (ATS -> S):** Same as `PeerReactToANIS` ATS -> S.
Live writer modes reset to INIT, OUT directory cleared. DEAD writers preserved
for `RSRestart`. On the legacy ANIS failover path (not produced by
`AdminStartFailover`), SYNC_AND_FWD writers could persist through ANISTS -> ATS
(`ANISTSToATS` does not snap writer modes); the reset covers that case too.
**ZK watcher dependency:** This is the critical transition that resolves the
non-atomic failover window. If lost: old active stays in ATS with mutations
blocked indefinitely (the (ATS, AIS) state persists). Safety holds (ATS maps to
ACTIVE_TO_STANDBY, `isMutationBlocked() = true`) but liveness requires eventual
watcher delivery. Curator `PathChildrenCache` re-queries on reconnect,
providing eventual delivery if the ZK session survives.
@@ -327,7 +327,9 @@ ANISToAIS(c) ==
## ANISTSToATS -- Drain Completion
-When the forwarder has drained the OUT directory and the anti-flapping gate
has opened, the cluster advances from ANISTS to ATS, joining the normal AIS
failover path. The standby reacts to ATS (not ANISTS), so this transition is
the bridge that lets the ANIS failover path converge with the AIS failover path.
+ANISTS is not produced by `AdminStartFailover` (failover requires AIS), so
this action is never enabled in the current model; it is kept to mirror
`setHAGroupStatusToSync()`'s ANISTS -> ATS mapping.
+
+When the forwarder has drained the OUT directory and the anti-flapping gate
has opened, the cluster advances from ANISTS to ATS, joining the normal AIS
failover path. The standby reacts to ATS (not ANISTS), so this transition is
the bridge that lets the legacy ANIS failover path converge with the AIS
failover path.
**Writer modes are NOT snapped here.** In the implementation,
`setHAGroupStatusToSync()` only writes the cluster-level ZK znode (ANISTS ->
ATS); it does not modify per-RS writer modes. SYNC_AND_FWD writers may persist
into ATS. They are cleaned up when the cluster transitions ATS -> S
(replication subsystem restart on standby entry -- see `PeerReactToAIS`,
`PeerReactToANIS`).
diff --git a/src/main/tla/ConsistentFailover/markdown/Types.md
b/src/main/tla/ConsistentFailover/markdown/Types.md
index f747389769..88dce1ca78 100644
--- a/src/main/tla/ConsistentFailover/markdown/Types.md
+++ b/src/main/tla/ConsistentFailover/markdown/Types.md
@@ -103,7 +103,7 @@ Each TLA+ abbreviation maps to a Java enum constant in
`HAGroupStoreRecord.HAGro
| `"AIS"` | `ACTIVE_IN_SYNC` | Active cluster, fully in sync with standby |
| `"ANIS"` | `ACTIVE_NOT_IN_SYNC` | Active cluster, at least one RS writing
locally (HDFS degraded) |
| `"ATS"` | `ACTIVE_IN_SYNC_TO_STANDBY` | Transitioning from active to standby
(mutations blocked) |
-| `"ANISTS"` | `ACTIVE_NOT_IN_SYNC_TO_STANDBY` | ANIS failover path: draining
OUT before advancing to ATS |
+| `"ANISTS"` | `ACTIVE_NOT_IN_SYNC_TO_STANDBY` | Legacy ANIS failover path
(not produced by `AdminStartFailover`): draining OUT before advancing to ATS |
| `"AbTAIS"` | `ABORT_TO_ACTIVE_IN_SYNC` | Aborting failover, returning to AIS
|
| `"AbTANIS"` | `ABORT_TO_ACTIVE_NOT_IN_SYNC` | Aborting failover, returning
to ANIS |
| `"AWOP"` | `ACTIVE_WITH_OFFLINE_PEER` | Active with offline peer. Reachable
when `UseOfflinePeerDetection = TRUE` |
@@ -236,7 +236,9 @@ AllowedTransitions ==
**ANIS self-transition** (`<<"ANIS", "ANIS">>`): This entry supports the
periodic heartbeat in `StoreAndForwardModeImpl` that refreshes the ZK znode's
`mtime` without changing the state value. In the TLA+ model, this maps to the
`ANISHeartbeat` action in [HAGroupStore.md](HAGroupStore.md), which resets the
anti-flapping countdown timer to `StartAntiFlapWait`. Source:
`HAGroupStoreRecord.java`.
-**DS -> STA** (`<<"DS", "STA">>`): This entry supports the ANIS failover path
where the standby is in `DEGRADED_STANDBY` when failover proceeds. The admin
initiates failover on the active (ANIS -> ANISTS), the forwarder drains OUT
(ANISTS -> ATS), and the standby detects ATS and transitions DS -> STA.
+**DS -> STA** (`<<"DS", "STA">>`): This entry covers a standby still in
`DEGRADED_STANDBY` when it observes the peer's ATS (e.g. it has not yet
observed the active's ANIS -> AIS recovery). Failover itself is only initiated
from AIS.
+
+**ANIS -> ANISTS** (`<<"ANIS", "ANISTS">>`): Mirrors
`HAGroupStoreRecord.java`, but no action produces it: `AdminStartFailover`
requires AIS, so ANISTS and its outgoing transitions are unreachable in the
model.
**AbTAIS -> ANIS** (`<<"AbTAIS", "ANIS">>`): This entry is needed so that HDFS
failure during the abort window can route the cluster to ANIS. Without it, S&F
writers that degrade during AbTAIS would have no path to a consistent state --
the cluster would be stuck in AbTAIS with degraded writers and no way for
`AutoComplete` to route to ANIS.
@@ -254,7 +256,7 @@ stateDiagram-v2
ANIS --> AIS : Recovery
ANIS --> ANIS : Heartbeat
- ANIS --> ANISTS : Admin failover
+ ANIS --> ANISTS : (unreachable; failover requires AIS)
ANIS --> ANISWOP : Peer offline
ATS --> S : Peer AIS/ANIS detected
diff --git a/src/main/tla/ConsistentFailover/markdown/Writer.md
b/src/main/tla/ConsistentFailover/markdown/Writer.md
index 58c6caf3e2..f9585d8da2 100644
--- a/src/main/tla/ConsistentFailover/markdown/Writer.md
+++ b/src/main/tla/ConsistentFailover/markdown/Writer.md
@@ -138,7 +138,7 @@ WriterInitToStoreFwd(c, rs) ==
### WriterSyncToSyncFwd -- Forwarder Started While In Sync: SYNC ->
SYNC_AND_FWD
-On an ACTIVE_NOT_IN_SYNC event, region servers currently in SYNC learn that
the cluster has entered ANIS and transition to SYNC_AND_FWD. This event fires
once when the cluster enters ANIS. ANISTS does not produce a new
ACTIVE_NOT_IN_SYNC event. A SYNC writer that has not yet received the event
when ANIS -> ANISTS fires will remain in SYNC (harmlessly: SYNC writers write
directly to standby HDFS, not to the OUT directory).
+On an ACTIVE_NOT_IN_SYNC event, region servers currently in SYNC learn that
the cluster has entered ANIS and transition to SYNC_AND_FWD. This event fires
once when the cluster enters ANIS. ANISTS does not produce a new
ACTIVE_NOT_IN_SYNC event. On the legacy ANIS -> ANISTS path (not produced by
`AdminStartFailover`), a SYNC writer that has not yet received the event
remains in SYNC (harmlessly: SYNC writers write directly to standby HDFS, not
to the OUT directory).
No ZK write -- mode transition driven by forwarder event.
