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/08/11 06:56:00 UTC

[jira] [Created] (HDDS-16128) Formal verification for Ozone multipart upload lifecycle with TLA+

Siyao Meng created HDDS-16128:
---------------------------------

             Summary: Formal verification for Ozone multipart upload lifecycle with TLA+
                 Key: HDDS-16128
                 URL: https://issues.apache.org/jira/browse/HDDS-16128
             Project: Apache Ozone
          Issue Type: Sub-task
            Reporter: Siyao Meng


Use TLA+ (via the Specula pipeline) to model and verify the Ozone OM multipart upload (MPU) lifecycle: initiate, commit part, complete, and abort, including FSO parent directory recreation and bucket quota (usedBytes and usedNamespace) accounting across the OM cache and the durable RocksDB state.

Model check the specification and validate real OM 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