[
https://issues.apache.org/jira/browse/HDDS-17540?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18134131#comment-18134131
]
Siyao Meng commented on HDDS-17540:
-----------------------------------
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: efe0c7eba1527530d1001f6517b733576fdc6d61
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: 4h 48m agent time, 78.2M tokens, about $48 (estimate)
{noformat}
h3. Result
10 candidate findings came out of model checking (1) and code review (9), and
all 10 were investigated individually.
||Disposition||Count||
|Reproduced|2|
|Masked (defect present, harm prevented by another component today)|1|
|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-29), and the fix patch, reproduction and
report were reviewed independently before filing. The review of the slot
priority issue found a second ordering that the first fix missed; the filed
patch covers both.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17559|Minor|EC decommission reconstruction can take a global
reconstruction slot while a container with a missing index waits for one|
|HDDS-17558|Minor|EC reconstruct commands rejected by the global reconstruction
limit are counted in EcReconstructionCmdsDeferredTotal as target datanode
deferrals|
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
* Masked: after a leader change the new leader can schedule the same
decommission index a second time, and over replication cleanup across a second
failover could remove every in service copy. This is a new way to reach the
open HDDS-16449 (pending ops cleared on leader change while an old term delete
still lands). The harm appeared only with a startup wait of 0 (not the default
5 minutes) plus nodes going stale between passes, the copy stayed on the
decommissioning node, and the next pass rebuilt it.
* False positive: global reconstruction slot release is tied to the ADD op
lifecycle. The over limit windows are bounded and the counter returns to 0; the
permanent leak needs a precondition no SCM path produces.
* False positive: the copy or reconstruct choice can flip between passes after
an ADD expires while the first command still runs. The duplicate does happen
and is cleaned up by over replication handling; no index is lost.
* False positive: the decommission reconstruction source check counts
maintenance and pending ADD indexes as sources. Reconstruction still reads from
healthy sources and never from the loaded node.
* False positive: a decommission reconstruct command can list the
decommissioning node as a source and an index as both source and target. The
datanode reader never reads an index it is told to rebuild, so the output is
correct.
* False positive: operational state is read from both the replica's persisted
state and the node status during admin transitions. The views disagree for
about one heartbeat and only delay work or add a harmless copy.
* False positive: {{isNodeHighlyLoaded}} treats unknown nodes and a limit of 0
or less as loaded. Both branches are unreachable, and switching all
decommission indexes costs no more than the alternative.
* False positive: a missing index and a decommission reconstruct command for
the same container in one pass take two global slots. The limit is honoured and
decommission falls back to a copy; it is a throughput question only.
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-ec-decommission-switch|apache/ozone|Java|Use the target-specific
guidance"
{code}
h3. Caveats
* Both issues need settings that are off by default
({{hdds.scm.replication.reconstruction.global.limit}} above 0, and for
HDDS-17559 also
{{hdds.scm.replication.decommission.ec.reconstruction.enabled}}), and both are
on master only, not in any release.
* HDDS-17559 was reproduced with unit tests that control when the
reconstruction holding the slot completes. How often it happens on a real
cluster depends on pass duration and the decommission backlog, which was not
measured. Nothing was run on a cluster.
* HDDS-17558 changes what {{EcReconstructionCmdsDeferredTotal}} counts on
master when a global limit is set.
* The patches were built and tested on the pinned commit and apply to master at
c7bd3772207. Both touch {{ReplicationManager}} and {{TestReplicationManager}};
they apply together in either order.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify scm-ec-decommission-switch (Apache Ozone master @efe0c7e)
> --------------------------------------------------------------------------
>
> Key: HDDS-17540
> URL: https://issues.apache.org/jira/browse/HDDS-17540
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: scm-ec-decommission-switch.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-ec-decommission-switch}}. Scope and code entry points are in the
> attached guidance file [^scm-ec-decommission-switch.guidance.md]. Added after
> HDDS-15071 and HDDS-15072 let SCM reconstruct EC indexes of decommissioning
> datanodes instead of copying them, under a global reconstruction limit.
> HDDS-16431 and HDDS-16535 covered EC replication and datanode admin before
> this change.
> h3. Run environment
> {noformat}
> Apache Ozone commit: efe0c7eba1527530d1001f6517b733576fdc6d61
> 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-ec-decommission-switch|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
> * 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]
