[
https://issues.apache.org/jira/browse/HDDS-16572?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18129877#comment-18129877
]
Siyao Meng commented on HDDS-16572:
-----------------------------------
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
Challenger debate, and severity classification.
h3. Run environment
{noformat}
Ozone commit: b10a7d427bdf83807a7e48a1be507d3b02d5a503
Specula: v1.2.0-34-gcdd19e39, with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 40G memory, 20 workers
Total: 5h 7m agent time, 126.2M tokens, about $70 (estimate)
{noformat}
h3. Result
14 candidate findings came out of model checking (10) and code review (4), and
all 14 were investigated individually.
||Disposition||Count||
|Reproduced|7|
|Masked (defect present, harm currently covered elsewhere)|5|
|False positive|2|
Each filed finding was 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-21), and the fix patch and report were reviewed
independently before filing. Findings that share a cause or a fix were filed
together.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17266|Minor|Reconcile container command is not resent when it is lost
before the datanode runs it (lost heartbeat reply, SCM leader change, datanode
restart)|
|HDDS-17267|Major|Datanode drops container CLOSE actions from heartbeats that
SCM did not process, so a full container can stay OPEN after an SCM restart|
|HDDS-17268|Major|Datanode ignores the heartbeat SCM term before term init and
updates it without the lock, so a stale SCM leader's command can run|
|HDDS-17269|Major|Datanode heartbeat queued behind a slow one runs after SCM
asks to reregister and drops pending container actions|
|HDDS-17279|Minor|Adding or removing an SCM on a running datanode can make
report producers throw, losing reports and stopping command status reports
until restart|
|HDDS-17280|Major|Datanode command processor thread busy-spins and SCM
heartbeats come too often while Recon or another endpoint keeps failing
GETVERSION|
|HDDS-17281|Minor|Datanode re-registration deletes the file of a running volume
health check, which can mark a healthy volume failed until restart|
Priorities follow the manual validation, not the pipeline's severity classes.
HDDS-17267 also covers one masked finding (actions lost on a failed heartbeat),
and HDDS-17269 covers two masked findings with the same cause (queued endpoint
tasks), because validation showed a reachable loss for them. HDDS-17268
combines two reproduced findings that need the same lock. Every issue except
HDDS-17266 has a proposed fix patch with regression tests and a standalone
reproduction test; HDDS-17266 has the reproduction only, because the fix needs
a design choice that is described in the issue.
h3. Not filed
* Masked: on a multi homed datanode each SCM's register response overwrites the
datanode's shared host name and address. No consumer acts on the overwritten
value at this commit.
* False positives: two findings (an exception between draining the queues and
sending the heartbeat, and non IO register errors) have no real trigger at this
commit.
* Found during validation, not filed: SCM HA followers skip CLOSE actions sent
before a new leader is ready. The gap closes by itself, because the next write
raises the CLOSE action again.
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=40G --tlc-worker-limit=20 \
"dn-registration|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17267 was also shown end to end in a mini cluster with a real SCM
restart; that run is not attached. For HDDS-17269 the full chain on a real
cluster (SCM restart under load, then a container that stays OPEN) was not run.
The wider impact of HDDS-17279 beyond the reproduced report loss is argued from
code.
* The patches were built and tested on the pinned commit and apply to master at
e0de543cbe9. HDDS-17267 and HDDS-17269 are independent and also apply together.
* HDDS-17267, HDDS-17268 and HDDS-17279 change StateContext and
HeartbeatEndpointTask, which open apache/ozone#11423 also changes; whichever
lands second will need a rebase.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify dn-registration (Apache Ozone master @b10a7d4)
> ---------------------------------------------------------------
>
> Key: HDDS-16572
> URL: https://issues.apache.org/jira/browse/HDDS-16572
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: dn-registration.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-registration}}. Scope and code entry points are in the attached guidance
> file [^dn-registration.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: b10a7d427bdf83807a7e48a1be507d3b02d5a503
> 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-registration|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]
