You are viewing a plain text version of this content. The canonical link for it is here.

Posted to issues@ozone.apache.org by "Siyao Meng (Jira)" <ji...@apache.org> on 2026/10/10 22:01:00 UTC

[jira] [Updated] (HDDS-16141) [Specula] Verify scm-delete-block (Apache Ozone master @9fbf9ee)

     [ https://issues.apache.org/jira/browse/HDDS-16141?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel ]

Siyao Meng updated HDDS-16141:
------------------------------
    Summary: [Specula] Verify scm-delete-block (Apache Ozone master @9fbf9ee)  (was: Formal verification for SCM delete-block transaction protocol with TLA+)

> [Specula] Verify scm-delete-block (Apache Ozone master @9fbf9ee)
> ----------------------------------------------------------------
>
>                 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: issues-unsubscribe@ozone.apache.org
For additional commands, e-mail: issues-help@ozone.apache.org