PHOENIX-7843 TLA+ specification of Consistent Failover#2461
Conversation
| @@ -0,0 +1,380 @@ | |||
| # Phoenix Consistent Failover -- TLA+ Specification | |||
|
|
|||
| Formal specification of the Phoenix Consistent Failover protocol using TLA+ and the TLC model checker. The spec verifies safety properties (mutual exclusion, zero RPO, abort correctness) under arbitrary interleavings of admin actions, HDFS failures, RS crashes, ZK connection/session failures, watcher retry exhaustion, and the anti-flapping timer. | |||
There was a problem hiding this comment.
This claims that the model is for verifying safety properties but at the end of this README file, it states that three liveness properties are also verified. Should we revise this statement?
|
|
||
| ### Post-Condition | ||
|
|
||
| Cluster `c` transitions to ATS or ANISTS, both of which map to the ACTIVE_TO_STANDBY role, blocking mutations (`isMutationBlocked() = true`). |
There was a problem hiding this comment.
This will change, shall I update it later when I make the implementation change? or do we want to right now? ANISTS will map to ACTIVE. This will optimize the failover time
|
|
||
| ## Overview | ||
|
|
||
| `HAGroupStore` models the peer-reactive transitions and auto-completion actions of the Phoenix Consistent Failover protocol. These actions correspond to the `FailoverManagementListener` (`HAGroupStoreManager.java` L633-706), which reacts to peer ZK state changes via `PathChildrenCache` watchers, and the local auto-completion resolvers from `createLocalStateTransitions()` (L140-150). |
There was a problem hiding this comment.
There is no discussion of SYSTEM.HA_GROUP system table. Is that intentional?
| \/ /\ clusterState[c] = "AbTAIS" | ||
| /\ clusterState' = [clusterState EXCEPT ![c] = | ||
| IF outDirEmpty[c] /\ \A rs \in RS : writerMode[c][rs] \in {"INIT", "SYNC"} | ||
| THEN "AIS" | ||
| ELSE "ANIS"] |
There was a problem hiding this comment.
This is not the implementation today. IIRC, this change is also not planned yet. Currently we go to AIS unconditionally as we expect the Active (A) cluster to be in a sync state when it moved to ATS so no new mutation has happened since then. Writer should handle AIS to ANIS transition once new write comes in.
|
|
||
| | TLA+ Action | Java Source | | ||
| |---|---| | ||
| | `AdminStartFailover(c)` | `HAGroupStoreManager.initiateFailoverOnActiveCluster()` L375-400 | |
There was a problem hiding this comment.
The line number citations can become stale, should we use a commit hash to pin these or we expect the reader to figure out from the method name?
3 participants
Formal specification of the Phoenix Consistent Failover protocol and implementation using TLA+ and the TLC model checker. The spec verifies safety properties such as mutual exclusion, zero RPO, and abort correctness under arbitrary interleavings of admin actions, HDFS failures, RS crashes, ZK connection/session failures, watcher retry exhaustion, and the anti-flapping timer.
Literate programming versions of all specification files are available in the
markdown/directory, referenced from theREADME.md. Each file includes the complete TLA+ code with comments converted to prose that discusses modeling choices, tradeoffs, and implementation traceability in depth.