[
https://issues.apache.org/jira/browse/HDDS-16570?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18133450#comment-18133450
]
Siyao Meng commented on HDDS-16570:
-----------------------------------
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: 6752db7978761a749a7d42a72a85311818e3d870
Specula: v1.2.0-35-gf5285a2b (with local changes)
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 2h 7m agent time, 63.6M tokens, about $45 (estimate)
{noformat}
h3. Result
10 candidate findings came out of model checking (4) and code review (6), and
all 10 were investigated individually.
||Disposition||Count||
|Reproduced|4|
|Environment limited (defect shown on the SCM side, end to end path needs
Kerberos)|1|
|Masked (defect present, harm prevented by another component today)|2|
|False positive|1|
|Already reported|2|
Each finding worth filing 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, and the fix patch, reproduction and report were reviewed
independently before filing. The environment limited finding and one reproduced
finding share one fix, so they are one issue.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17519|Major|After a long SCM pause the node health checker marks live
datanodes STALE or DEAD, as it skips only one run and misses some pauses|
|HDDS-17518|Minor|StaleNodeHandler closes pipelines of a datanode that is
HEALTHY again when it handles a late STALE_NODE event|
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
* Reproduced, same defect as HDDS-16633 (open apache/ozone#11688, which already
contains the fix): when a datanode re-registers with a changed address, ports
or version between the health checker's read and its write, the checker writes
DEAD onto the fresh entry and {{DeadNodeHandler}} runs on the live datanode.
HDDS-16633 describes only the opposite ordering. If the handler runs after the
registration's container report, SCM forgets the datanode's replicas until the
next full report. A regression test for this ordering is available for that PR.
* Reproduced, already reported as HDDS-17425: with apache/ozone#11692 applied,
an older software datanode that is STALE at finalize is restored to HEALTHY and
never fenced.
* Already reported: a heartbeat between the checker's TIMEOUT and RESTORE steps
(HDDS-17229), and the version report stored before the fence check (HDDS-16798,
HDDS-17425).
* Masked: a DEAD datanode that re-registers with a changed version or ports
becomes HEALTHY without the UNHEALTHY_TO_HEALTHY_NODE event. Its only
subscriber wakes {{BackgroundPipelineCreator}}, which also runs every 120s.
* Masked: a node removed during a health check pass aborts the rest of that
pass. Only Recon's admin remove endpoint removes nodes, and the next pass, one
checker interval later, corrects the skipped nodes.
* False positive: an unhandled runtime exception stopping the health checker.
No reachable source of one was found.
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 \
"scm-node-health|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17519 was run on a real SCM with the existing pause hook and scaled
timings, with heartbeats lost during the pause modelled by not sending them.
Which datanodes lose heartbeats on a real transport was read from the code, not
run: with Kerberos the handshake cannot complete during the pause, and with
SIMPLE authentication mainly the pause just under the stale interval applies.
The patch delays marking a really dead datanode by about 35s after a detected
pause, and for Recon, which datanodes heartbeat every 60s, it narrows the gaps
without closing them.
* HDDS-17518 was run at unit level with the event delivery order chosen by the
test. How far the STALE_NODE handler can lag on a real cluster was not measured.
* Mini cluster suites were not run for either patch.
* The patches were built and tested on the pinned commit and apply to master at
9118d5a85a3. The HDDS-17519 patch applies on top of apache/ozone#11688 and
conflicts textually with the draft apache/ozone#11349, which changes the clock
reads in the same methods.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify scm-node-health (Apache Ozone master @6752db7)
> ---------------------------------------------------------------
>
> Key: HDDS-16570
> URL: https://issues.apache.org/jira/browse/HDDS-16570
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: scm-node-health.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
> {{scm-node-health}}. Scope and code entry points are in the attached guidance
> file [^scm-node-health.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: 6752db7978761a749a7d42a72a85311818e3d870
> 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 \
> "scm-node-health|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]
