[
https://issues.apache.org/jira/browse/HDDS-16123?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18125908#comment-18125908
]
Siyao Meng commented on HDDS-16123:
-----------------------------------
Verification run complete. The om-quota-repair target ran through the full
Specula pipeline at Ozone 9fbf9ee0cb1bd2f5f5d437b6719ebbe5309351fb
(claude-code, Claude Opus 4.8, effort max).
h3. Result
Four findings came out of model checking (3) and code review (1).
||Finding||Disposition||Issue||
|MC-2|Reproduced, High|HDDS-16125|
|MC-3|Reproduced, High|HDDS-16126|
|CR-3|Reproduced, High|HDDS-16127|
|MC-1|Masked, High|Not filed|
MC-1: a repair delta applied twice on an unflushed baseline can drive
{{usedBytes}} negative. Leader only routing of {{StartQuotaRepair}} and the in
progress fence mask it today, so it was not filed.
h3. Follow ups
HDDS-16175, HDDS-16176, HDDS-16177, HDDS-16178 and HDDS-16184 were found by
code analysis while scoping the fix for HDDS-16127 (at Ozone 4766aa8609), not
by the pipeline. They are linked here as well.
Resolving as Done.
> [Specula] Verify om-quota-repair (Apache Ozone master @9fbf9ee)
> ---------------------------------------------------------------
>
> 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]
