apurtell opened a new pull request, #2461: URL: https://github.com/apache/phoenix/pull/2461
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 the `README.md`. Each file includes the complete TLA+ code with comments converted to prose that discusses modeling choices, tradeoffs, and implementation traceability in depth. -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected]
