Andrew Kyle Purtell created PHOENIX-7843:
--------------------------------------------
Summary: TLA+ specification of Consistent Failover
Key: PHOENIX-7843
URL: https://issues.apache.org/jira/browse/PHOENIX-7843
Project: Phoenix
Issue Type: Task
Reporter: Andrew Kyle Purtell
Assignee: Andrew Kyle Purtell
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.
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
