[
https://issues.apache.org/jira/browse/HDDS-16575?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18130331#comment-18130331
]
Siyao Meng commented on HDDS-16575:
-----------------------------------
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: 07512078fe639f387acd52104491d5a7f3edb84c
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: 3h 45m agent time, 68.8M tokens, about $50 (estimate)
{noformat}
h3. Result
12 candidate findings came out of model checking (4) and code review (8), and
all 12 were investigated individually. One model checking finding went through
three spec repair rounds before it was classed as a false positive.
||Disposition||Count||
|Reproduced|2|
|Masked (defect present, harm prevented by another component today)|2|
|False positive|7|
|Already reported (HDDS-16804)|1|
The two reproduced findings share one root cause and one fix, so they are one
issue. One masked finding is filed as well, because its one line fix is cheap
and its effect, although small, reaches operators. 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-22), and the fix patch, reproduction and report were reviewed
independently before filing.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17331|Minor|Concurrent node state change and replication streams limit
reconfiguration can leave the datanode replication pool at the wrong size or
throw|
|HDDS-17330|Minor|ReplicationSupervisorMetrics can throw
ConcurrentModificationException when the first task of a new type is added
during a metrics snapshot|
Priorities follow the manual validation, not the pipeline's severity classes
(High for both parts of HDDS-17331, Medium for HDDS-17330). Each issue has a
proposed fix patch and a standalone reproduction test attached.
h3. Not filed
* Masked: {{ReplicationSupervisor.stop}} drops the list returned by
{{shutdownNow}}, so tasks still queued keep their in flight and counter
entries. It is only called when the datanode stops, and the stopped supervisor
is never reused.
* False positive (7): a late per volume task after a volume failure (after
three spec repair rounds), a negative container ID that SCM cannot produce,
concurrent command handling that the single command processor thread rules out,
an unsynchronized read of the SCM leader term with no observable effect on the
term check, outcome counters that no consumer relies on to balance, a test only
helper, and the exactly once release of a task across the volume failure and
rejection paths.
* Already reported: a dedupe drop when an equal task absorbs a new command,
tracked in HDDS-16804.
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 \
"dn-replication-supervisor|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17331 needs an SCM node state change and an admin reconfiguration of the
streams limit on the same datanode within a window of a few calls. The
reproductions hold one thread at the existing {{executorThreadUpdater}} builder
hook. Without the hook, two plain threads lost the update 4 times in 20000
iterations, and the exception was seen only under extra CPU load. The bug is in
master only (HDDS-10237).
* HDDS-17330 can happen at most twice per datanode process. The reproduction
forces the overlap on the snapshot thread. A run with real timing was not
attempted.
* All reproductions ran as {{hadoop-hdds/container-service}} tests, not on a
running cluster.
* The patches were built and tested on the pinned commit and apply to master at
2851f5a3057. Both touch {{ReplicationSupervisor}} and
{{TestReplicationSupervisor}}, and they apply on top of each other in either
order.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify dn-replication-supervisor (Apache Ozone master @0751207)
> -------------------------------------------------------------------------
>
> Key: HDDS-16575
> URL: https://issues.apache.org/jira/browse/HDDS-16575
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: dn-replication-supervisor.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
> {{dn-replication-supervisor}}. Scope and code entry points are in the
> attached guidance file [^dn-replication-supervisor.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: 07512078fe639f387acd52104491d5a7f3edb84c
> 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 \
> "dn-replication-supervisor|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]
