[
https://issues.apache.org/jira/browse/HDDS-16141?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Siyao Meng reassigned HDDS-16141:
---------------------------------
Assignee: Siyao Meng
> 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
> Assignee: Siyao Meng
> Priority: Major
>
> 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]
