[
https://issues.apache.org/jira/browse/HDDS-16547?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18127453#comment-18127453
]
Siyao Meng commented on HDDS-16547:
-----------------------------------
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: 0665932dd35da4d05087e02748af0a64eb846ad5
Specula: v1.0.0-63-g54fe3a93 (with local changes)
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 3h 49m agent time, 133.1M tokens, about $84 (estimate)
{noformat}
h3. Result
18 candidate findings came out of model checking (7) and code review (11), and
all 18 were investigated individually.
||Disposition||Count||
|Reproduced|12|
|Masked (defect present, harm prevented by another component today)|2|
|False positive|2|
|Dropped (already reported)|2|
Three reproduced findings share one root cause and one fix, so they are one
issue. Each issue 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-15), and the fix patch, reproduction and report were
reviewed independently before filing. One of the two masked findings is filed
as well, because the component that masks it does so with a full rebuild of
every Recon OM task, and an ordinary bucket cleanup triggers it.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17044|Major|Recon unlinks a renamed FSO directory in the namespace
summary when the rename's PUT event is processed before its DELETE|
|HDDS-17045|Major|Recon adds a Legacy directory's totals to its ancestors again
on every in place update of the directory key, such as an ACL change|
|HDDS-17048|Major|Recon NSSummary task fails with NullPointerException on a key
event whose bucket is already deleted in the Recon OM DB, forcing a full
rebuild|
|HDDS-17049|Major|Recon counts keys of a recreated bucket under the deleted
bucket after a delete and recreate in one OM flush or behind a rebuild|
|HDDS-17042|Major|Recon manual task rebuild requested while a delta sync is
being applied makes the tasks apply that delta twice|
|HDDS-17041|Minor|Retry of a failed NSSummaryTask applies namespace summary
deltas twice or skips them, so Recon file counts and sizes stay wrong|
|HDDS-17043|Minor|Recon emits a second DELETE event with a stale value when a
key is deleted twice within one delta sync, and subtracts the key twice|
|HDDS-17050|Minor|Recon task cursor advances past a batch that failed both
attempts, so a restart soon after the failure can lose that batch|
|HDDS-17040|Minor|Recon delta task that throws is not retried and triggers no
reinitialization, so its batch is silently skipped|
|HDDS-17046|Minor|An Error during the Recon NSSummary rebuild leaves the
rebuild state RUNNING, so every later rebuild is skipped until restart|
|HDDS-17047|Minor|Failed rename while Recon swaps in its rebuilt DB leaves no
open DB; Recon DB reads and later rebuilds fail until restart|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch and a standalone reproduction test attached.
h3. Not filed
* Masked: a staged NSSummaryTask that loses the shared rebuild state check
reports success without rebuilding. Every production rebuild goes through the
synchronized controller method, which serializes them, so this was only shown
by calling two staged instances directly.
* Already reported: a crash between the Recon OM DB write and the delta cursor
save leaves the batch unapplied (HDDS-5146, still open).
* Already reported: the Legacy parent lookup throws when the parent directory
key is deleted in the same batch, forcing a rebuild (HDDS-10855, behaviour kept
on purpose).
* False positive: after a reinitialize the namespace summary manager publishes
its DB handles through non volatile fields. No stale read was observed, so the
suggested change is hardening only.
* False positive: a deleted bucket's summary row is never removed. OM only
deletes empty buckets, so the row holds zeros, and every reader looks rows up
by an objectID from live OM state, so it is never read.
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 \
"recon-namespace-summary|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17044, HDDS-17043, HDDS-17045 and HDDS-17048 were reached with ordinary
client operations and no fault injection. HDDS-17045 needs
{{ozone.om.enable.filesystem.paths=true}}. HDDS-17044 leaves one case unfixed:
two renames in one OM flush that swap nesting, which needs the events delivered
in order; the patch does not make that case worse.
* HDDS-17041, HDDS-17040 and HDDS-17046 need a failure that the reproductions
inject. For HDDS-17041 the natural transient source is argued from code, not
run, and the window is narrow. A Recon RocksDB I/O error is not a trigger for
any of them, because the DB closes itself and the resulting rebuild covers the
loss.
* HDDS-17042 needs a manual rebuild request during a delta sync; the upgrade
actions cannot race because they run before the sync starts. HDDS-17050 needs a
restart within about one sync interval of the failure while OM has new writes.
HDDS-17047 needs a rename to fail during the DB swap, which is hard to reach
because a failing {{.backup}} delete normally stops the swap first.
* Two patches change behaviour beyond the bug: with HDDS-17040 a task that
throws on every attempt leads to a full reinitialization, as a task that
returns failure already does; with HDDS-17047 a failed DB swap queues another
rebuild instead of reporting success.
* The patches were built and tested on the pinned commit and apply to master at
2264d4d48ac. All eleven apply together except that the patches of HDDS-17041
and HDDS-17048 add tests at the same place in {{TestNSSummaryTask}}, so the
second one to land needs a trivial rebase.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify recon-namespace-summary (Apache Ozone master @0665932)
> -----------------------------------------------------------------------
>
> Key: HDDS-16547
> URL: https://issues.apache.org/jira/browse/HDDS-16547
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: recon-namespace-summary.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
> {{recon-namespace-summary}}. Scope and code entry points are in the attached
> guidance file [^recon-namespace-summary.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: 0665932dd35da4d05087e02748af0a64eb846ad5
> 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 \
> "recon-namespace-summary|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]