Siyao Meng created HDDS-16123:
---------------------------------
Summary: Formal verification for OM quota accounting and online
repair
Key: HDDS-16123
URL: https://issues.apache.org/jira/browse/HDDS-16123
Project: Apache Ozone
Issue Type: Sub-task
Reporter: Siyao Meng
Formal/semi-formal verification of the OM quota accounting and online
quota-repair path, using TLA+ trace validation and model checking against
Apache Ozone at commit 9fbf9ee0cb1bd2f5f5d437b6719ebbe5309351fb.
Scope: QuotaRepairTask (checkpoint baseline plus additive delta, parallel
scans, concurrent mutation, distributed run fencing, bucket identity), and the
quota accounting it reconciles (cache versus durable coherence, versioned-key
and multipart size accounting).
Findings are filed as separate bugs linked to this issue via "Testing
discovered".
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
