[
https://issues.apache.org/jira/browse/HDDS-16473?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18125242#comment-18125242
]
Siyao Meng commented on HDDS-16473:
-----------------------------------
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: a6332fb59879b80615b9233e953d6813d03ae7a8
Specula: v1.2.0 plus 24 commits (6190c183)
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 2h 41m agent time, 71.3M tokens, about $60 (estimate)
{noformat}
h3. Result
7 candidate findings came out of model checking (5) and code review (2), and
all 7 were investigated individually.
||Disposition||Count||
|Reproduced|6|
|False positive|1|
Each reproduced finding 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-10-08), and the fix patch, reproduction and
report were reviewed independently before filing. All 6 held up and each needs
its own fix, so 6 issues are filed. One further defect in the same accounting,
found during that review rather than by the pipeline, was validated the same
way and is filed as a seventh issue.
h3. Filed
||Issue||Priority||Summary||
|HDDS-16795|Major|KeyDeletingService can purge keys twice after a leader change
to an OM still applying a backlog, or after an OM restart|
|HDDS-16792|Major|Deleting a key that a stale overwrite commit recreated
replaces its pending deletedTable entry, so the blocks of one version are never
deleted|
|HDDS-16791|Major|PurgeKeys requests that only carry keysToUpdate are rejected,
so a partly reclaimable deleted key is not rewritten and its blocks are resent
to SCM|
|HDDS-16793|Major|Quota repair adds deletedTable entries without the committed
flag to the pending deletion usage of the bucket, and the purge never releases
them|
|HDDS-16796|Major|deletedTable entries inherit the committed flag from their
key info, so the purge can release pending deletion usage that was never added|
|HDDS-16794|Minor|KeyDeletingService run that outlives a lost and regained OM
leadership purges keys again and reduces bucket usage twice|
|HDDS-16790|Minor|KeyDeletingService can purge a deleted key in one PurgeKeys
request and carry its size in another, leaving the size in the bucket usage for
good|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch attached, and all but HDDS-16796 also have
a standalone reproduction test. HDDS-16796 is the issue found during review;
its two regression tests are in its patch.
h3. Not filed
* False positive: a block group without an SCM result is treated as neither
success nor failure by the purge decision. It needs an SCM response with fewer
results than block groups, which no SCM code path produces.
h3. Reproduce
{code:none}
specula run --agent=claude-code --effort=medium --model='claude-opus-5-5[1m]' \
--max-parallel=2 --enable-reviews --confirm-debate \
--tlc-memory-limit=28G --tlc-worker-limit=8 \
"om-aos-key-deletion|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* All reproductions ran against one real OM or a mini cluster with a recording
SCM block client. Effects on SCM and datanodes (repeated delete transactions,
blocks left on datanodes) are argued from the code.
* HDDS-16795 needs a run to start between leader ready and the moment the OM
has applied its backlog. The reproduction holds the replay open after a
restart. The leader change form is argued, not run. The snapshot tasks have the
same weakness and are not covered by the patch.
* HDDS-16794 needs one run to stall across two leadership changes. Its patch
was reworked after review into a smaller change that narrows the window and
does not close it, and it names the stricter alternative.
* HDDS-16790 needs deleted key names of about 600 bytes on average in one run
at default limits. The reproduction forces the split with a small Ratis limit.
* HDDS-16793 affects unreleased master only (the recount came with HDDS-15204).
* HDDS-16792 changes how new deletedTable entries are named, without a layout
feature, as HDDS-10296 did.
* HDDS-16796 and HDDS-16793 touch the same accounting. HDDS-16793's patch
pre-sets the flag on a shared test fixture that HDDS-16796 then decides, so the
second of the two to land carries that fixture line over.
* The patches were built and tested on the pinned commit and apply to master at
fa7b58e3901. They are otherwise independent, and all seven apply on one tree
except that HDDS-16795 and HDDS-16790 touch the same test imports, so the
second of those two to land needs a trivial rebase.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-aos-key-deletion (Apache Ozone master @a6332fb)
> -------------------------------------------------------------------
>
> Key: HDDS-16473
> URL: https://issues.apache.org/jira/browse/HDDS-16473
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: om-aos-key-deletion.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-aos-key-deletion}}. Scope and code entry points are in the attached
> guidance file [^om-aos-key-deletion.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: a6332fb59879b80615b9233e953d6813d03ae7a8
> 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-aos-key-deletion|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 ({{20e6a1c}}); 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
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
