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