[jira] [Commented] (HDDS-16123) [Specula] Verify om-quota-repair (Apache Ozone master @9fbf9ee)

["Siyao Meng (Jira)" <ji...@apache.org>]

    [ 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: issues-unsubscribe@ozone.apache.org
For additional commands, e-mail: issues-help@ozone.apache.org