[
https://issues.apache.org/jira/browse/HDDS-17640?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18136498#comment-18136498
]
Siyao Meng commented on HDDS-17640:
-----------------------------------
Verification run complete. The Specula pipeline ran all phases against the
pinned commit: code analysis, TLA+ specification generation, harness and trace
collection, trace validation plus TLC model checking, bug confirmation with the
adversarial Challenger debate, and severity classification.
h3. Run environment
{noformat}
Ozone commit: ec5ed5f7ea0e4b406aee53aae4906616819cba2b
Specula: v1.2.0-35-gf5285a2b (with local changes)
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 40G memory, 20 workers
Ran on: a Linux lab host, on the Claude subscription
Total: 5h 43m agent time, 149.3M tokens, about $72 (estimate)
{noformat}
h3. Result
6 candidate findings came out of model checking (3) and code review (3), and
all 6 were investigated individually. No spec repair requests were raised by
confirmation.
||Disposition||Count||
|Reproduced|3|
|Dropped (already reported upstream)|2|
|False positive|1|
Two reproduced findings share one root cause and one fix, so they are one
issue. It was then validated a second time by hand against the pinned commit: a
regression test was added to an existing suite and shown to fail without the
fix and pass with it, the bug was confirmed still present on apache master
(checked on 2026-11-02), and the fix patch, reproduction and report were
reviewed independently before filing. The third reproduced finding is an
existing open issue and is not filed again.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17670|Minor|DirectoryDeletingService run that outlives a lost and
regained OM leadership purges directories again and reduces bucket usage twice|
Priorities follow the manual validation, not the pipeline's severity classes
(the pipeline classed all three reproduced findings as Critical). The issue has
a proposed fix patch and a standalone reproduction test attached.
h3. Not filed
* Reproduced, already reported as HDDS-16792 (open): a second delete of a key
recreated by an overwrite commit replaces the first version's {{deletedTable}}
entry. Reproduced again at this commit with ordinary client requests on FSO and
object store buckets. The patch attached to HDDS-16792 fixes it at this commit
on every delete path tried (DeleteKey, DeleteKeys, a delete between the
{{KeyDeletingService}} scan and its purge, a snapshot taken before the first
delete, a recursive delete of the parent directory); it needs {{git apply
--3way}} because of one import hunk in {{TestKeyDeletingService}}.
* Dropped, already reported as HDDS-17248 (open).
* Dropped, already reported as HDDS-16796 (open).
* False positive: the quota repair task recomputes the same bucket counters as
the runtime paths on the paths tested.
h3. Reproduce
{code:none}
specula run --agent=claude-code --effort=medium --model='claude-opus-5-5[1m]' \
--max-parallel=4 --enable-reviews --confirm-debate \
--tlc-memory-limit=40G --tlc-worker-limit=20 \
"om-quota-accounting|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17670 needs the thread of one service run to stall across two leadership
changes and the run of the other leader, up to about a minute with the default
interval. The reproduction holds the submit of a second service instance on a
latch; a stall of that length in production is argued, not measured.
* The HDDS-17670 patch narrows the window and does not close it, like the patch
on HDDS-16794 for {{KeyDeletingService}}. The two patches change different
files and apply together on the pinned commit; if both are taken, the term
check can move into {{AbstractKeyDeletingService}}.
* The patch was built and tested on the pinned commit and applies to master at
6ab9ed82a81.
* The patch is a proposal for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-quota-accounting (Apache Ozone master @ec5ed5f)
> -------------------------------------------------------------------
>
> Key: HDDS-17640
> URL: https://issues.apache.org/jira/browse/HDDS-17640
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: om-quota-accounting.guidance.md
>
>
> This is a runnable Apache Ozone formal-verification target for the Specula
> pipeline (TLA+ model checking plus trace validation against the real code).
> It has not been run yet. Anyone can pick it up: run Specula against the
> pinned commit, then report findings on this issue. Part of umbrella
> HDDS-15926.
> h3. Target
> {{om-quota-accounting}}. Scope and code entry points are in the attached
> guidance file [^om-quota-accounting.guidance.md]. Added because no run has
> targeted quota accounting itself, while runs on other targets keep finding
> quota leaks on the side (HDDS-16773, HDDS-17240, HDDS-16117, HDDS-16787); the
> earlier om-quota-repair run (HDDS-16123) covered only the repair task.
> h3. Run environment
> {noformat}
> Apache Ozone commit: ec5ed5f7ea0e4b406aee53aae4906616819cba2b
> Specula: https://github.com/specula-org/Specula (v1.1.0 or later)
> Toolchain: JDK 21, ~28 GB RAM for TLC, an LLM coding agent
> (claude-code or codex adapter)
> Runtime: hours per target; needs an agent API budget
> {noformat}
> h3. How to run
> # Clone Specula and install per its README; clone apache/ozone and check out
> the pinned commit above.
> # Place the attached guidance file as the target's .prompt-extra.md (see the
> Specula README for target layout).
> # Run:
> {code:none}
> specula run --agent=claude-code --effort=medium --keep-original
> --max-parallel=2 \
> --enable-reviews --confirm-debate --tlc-memory-limit=28G
> --tlc-worker-limit=8 \
> "om-quota-accounting|apache/ozone|Java|Use the target-specific
> .prompt-extra.md"
> {code}
> # Deliverables land under the run's {{.specula-output/}}:
> {{confirmed-bugs.md}}, {{bug-severity.md}}, {{summary.md}}, and
> {{confirmation/<id>/investigation.md}}.
> h3. Reporting results
> Comment here with the outcome (0 findings is still useful: it records the
> target as covered at this commit). For each confirmed bug, file a separate
> Ozone Bug and link it to this issue with the "Testing" link type ("Testing
> discovered").
> h3. Notes
> * The attached guidance file names an earlier commit ({{ef63bac}}); use the
> commit above. Code entry-point line numbers in the guidance were captured at
> an earlier commit and may have shifted on this head; treat them as
> approximate. Specula re-analyzes the source, so the run does not depend on
> them.
> * Recon-building targets need a local Specula patch to skip Maven {{target/}}
> out-of-tree symlinks in {{snapshotlib._validate_source_tree}}, else the run
> crashes at finalize.
> * effort=medium is the tested default for large targets; effort=high can hit
> per-turn timeouts on the biggest ones.
> * Findings are proposals, to be confirmed by human review and testing before
> any fix is merged.
--
This message was sent by Atlassian Jira
(v10.3.26#10030026)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
