[
https://issues.apache.org/jira/browse/HDDS-16578?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18130843#comment-18130843
]
Siyao Meng commented on HDDS-16578:
-----------------------------------
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, one scoped repair round, and severity
classification.
h3. Run environment
{noformat}
Ozone commit: fb2d0310a9c6ea37c72cefb5cc1d5b4db35a7ab1
Specula: v1.2.0-34-gcdd19e39 (with local changes)
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 2h 17m agent time, 47.3M tokens, about $40 (estimate)
{noformat}
h3. Result
13 candidate findings came out of model checking (6) and code review (7), and
all 13 were investigated individually. One repair round refined the
specification after the first confirmation pass and the five model checking
violations were confirmed again against it.
||Disposition||Count||
|Reproduced|6|
|Masked (defect present, harm prevented by another component today)|1|
|False positive|6|
Two 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-23), and the fix patch, reproduction and report were
reviewed independently before filing. The masked finding is filed as well,
since only the Recon web interface masks it.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17389|Major|Recon export cleanup deletes every directory and .tar file in
ozone.recon.export.directory, not only files created by exports|
|HDDS-17390|Major|ExportJobManager registers an export task only after handing
it to the worker, so cancelJob and the worker's cleanup can miss it|
|HDDS-17391|Major|Recon export job that fails to create its working directory
keeps its queue slot, so later exports are rejected as "queue is full"|
|HDDS-17392|Minor|Recon export job stays RUNNING forever after an Error such as
OutOfMemoryError, and new exports for its state are rejected|
|HDDS-17393|Minor|Description of ozone.recon.export.max.jobs.total says it
counts the executing export job, but only waiting jobs are counted|
|HDDS-17388|Minor|Recon unhealthy container export returns 429 Too Many
Requests for a duplicate export, which retrying never clears|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch attached, and all but HDDS-17390 also have
a standalone reproduction test.
h3. Not filed
* False positive: after a restart of the manager inside one JVM the old worker
can still publish an archive. Nothing in Recon recreates the manager within a
running process.
* False positive: the archive is written at its final name without a temporary
name and rename. Nothing reads an archive before its job is COMPLETED, and
every failure path removes it.
* False positive: a job removed between the download check and the lazy file
open. Run end to end, it showed neither a broken response body nor a lost
download slot.
* False positive: {{ExportJob}} status and counters are plain fields written by
two threads. The data race is real under the Java memory model, but no reader
can observe a harmful stale value.
* False positive: FAILED jobs are kept until they are deleted. That is the
designed job history.
* False positive: stale Javadoc for the default export directory. It is never
read at runtime, and {{ozone-default.xml}} gives the correct default.
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-export-jobs|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* All reproductions run {{ExportJobManager}} in unit tests with the database
layer mocked, not in a full Recon deployment.
* HDDS-17390 depends on a short window between handing the task to the worker
and registering it. Its regression tests fix the order of steps with a worker
pool replaced by reflection; it has no separate standalone reproduction.
Without that, a concurrent in process test hit the cancel case in most of 300
runs, and the stale registration in 19 of 20000 submissions on a loaded host.
* HDDS-17391 needs the export directory to be unwritable when a job starts, for
example after wrong permissions or a read only remount, or not created at
startup, which Recon only logs.
* HDDS-17392 needs an Error such as OutOfMemoryError in the export worker of a
Recon process that keeps running. Its reproduction throws the error from the
mocked database layer; a real heap exhaustion was not run.
* HDDS-17389 needs a non default {{ozone.recon.export.directory}}. The default
location only ever holds export files.
* HDDS-17393 corrects the description of {{ozone.recon.export.max.jobs.total}}
and does not change the limit.
* The patches were built and tested on the pinned commit, and each applies to
master at 9c3e5477ffb. On the pinned commit they apply together in any order
except that HDDS-17389 and HDDS-17388 each conflict with HDDS-17390 in import
lines of {{ExportJobManager}} and {{TestExportJobManager}}, so whichever lands
second needs a trivial rebase.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify recon-export-jobs (Apache Ozone master @fb2d031)
> -----------------------------------------------------------------
>
> Key: HDDS-16578
> URL: https://issues.apache.org/jira/browse/HDDS-16578
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: recon-export-jobs.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-export-jobs}}. Scope and code entry points are in the attached
> guidance file [^recon-export-jobs.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: fb2d0310a9c6ea37c72cefb5cc1d5b4db35a7ab1
> 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-export-jobs|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
(v10.3.26#10030026)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
