Siyao Meng created HDDS-16141:
---------------------------------
Summary: Formal verification for SCM delete-block transaction
protocol with TLA+
Key: HDDS-16141
URL: https://issues.apache.org/jira/browse/HDDS-16141
Project: Apache Ozone
Issue Type: Sub-task
Reporter: Siyao Meng
Use TLA+ (via the Specula pipeline) to model and verify the SCM delete-block
transaction protocol: deleted-block log durability, per-datanode command state,
ACK and timeout handling, transaction retry and resend, replica-set membership
at removal, the volatile deleted-block transaction summary accounting, and
volatile-state reconstruction after SCM leader transfer, across the SCM HA
transaction buffer and the durable RocksDB state.
Model check the specification and validate real SCM traces against it. Bugs
found by this effort are linked under this issue.
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
