[
https://issues.apache.org/jira/browse/HDDS-16535?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18129476#comment-18129476
]
Siyao Meng commented on HDDS-16535:
-----------------------------------
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: b0aa6475b7856d2c7f467dd3db12b9a1dd116f63
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: 8h 59m agent time, 173.7M tokens, about $104 (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|11|
|False positive|7|
Each reproduced finding 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-21), and the fix patch and report were
reviewed independently before filing. Two further defects were found during
that review and are filed as well (HDDS-17226, HDDS-17228).
h3. Filed
||Issue||Priority||Summary||
|HDDS-17224|Major|Decommission or maintenance completes on an empty container
set after SCM restart or datanode re-registration, before the full container
report|
|HDDS-17225|Major|Decommission completes while a container on the node is under
replicated but recorded under a combined state such as
UNHEALTHY_UNDER_REPLICATED|
|HDDS-17222|Major|Decommission or maintenance never completes if the datanode
registers again with a new version or ports before SCM sees its persisted state|
|HDDS-17223|Major|A datanode that registers again with a new address, version
or ports overwrites the operational state held by the leader SCM|
|HDDS-17220|Major|Decommission or maintenance requested while a recommission is
still queued is acknowledged and then lost, and the datanode returns to
IN_SERVICE|
|HDDS-17226|Major|A recommission is silently lost when the datanode admin
workflow is resumed before the next monitor run, and the cancelled request
completes|
|HDDS-17229|Major|A heartbeat that arrives while SCM marks a stale datanode
DEAD leaves it HEALTHY but missing from the network topology|
|HDDS-17227|Major|A failed rewrite of datanode.id leaves it empty, so the
datanode loses its operational state and initial version on the next start|
|HDDS-17228|Major|A failed rewrite of a VERSION file publishes the empty
temporary file, so SCM, OM or a datanode cannot start again|
|HDDS-17218|Minor|Datanode can enter maintenance below the replica minimum
because a replica on a STALE datanode still counts as an available copy|
|HDDS-17219|Minor|Decommission monitor on a stepped down SCM can overwrite the
operational state reported by a datanode, so a later re-promotion drops the
decommission|
|HDDS-17221|Minor|Starting maintenance again on a datanode already in
maintenance reports success but keeps the old maintenance end|
|HDDS-17217|Minor|A failed pipeline close at the start of decommission or
maintenance is never retried, so the datanode waits for its pipeline
indefinitely|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch with a regression test and a standalone
reproduction test attached. HDDS-17224 is related to the open HDDS-16632, which
covers the re-registration variant; the SCM restart variant had no issue.
h3. Not filed
* The seven false positives were judged not to hold on a running SCM: transient
mismatches that the next heartbeat or monitor run corrects by design,
containers SCM has no record of and could not repair anyway, and races whose
outcome is the same as the decision the leader makes on its next run.
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 \
"scm-datanode-admin|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* Patches that change the same lines: HDDS-17223 depends on HDDS-17222 and must
not land without it. HDDS-17221 and HDDS-17226 each overlap HDDS-17220 on one
hunk, and the second to land needs that hunk refreshed. HDDS-17228 applies the
HDDS-17227 fix to a second helper, with no ordering dependency.
* HDDS-17219 applies to master with a three way merge; the other patches apply
to master at 20d95ed37fe unchanged.
* SCM HA failover and multi SCM behaviour were argued from code and single SCM
tests; no three SCM cluster was run.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5 and Claude Opus 5).
> [Specula] Verify scm-datanode-admin (Apache Ozone master @b0aa647)
> ------------------------------------------------------------------
>
> Key: HDDS-16535
> URL: https://issues.apache.org/jira/browse/HDDS-16535
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: scm-datanode-admin.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-datanode-admin}}. Scope and code entry points are in the attached
> guidance file [^scm-datanode-admin.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: b0aa6475b7856d2c7f467dd3db12b9a1dd116f63
> 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-datanode-admin|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]
