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: [email protected]
For additional commands, e-mail: [email protected]
