[
https://issues.apache.org/jira/browse/HDDS-17566?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18135444#comment-18135444
]
Siyao Meng commented on HDDS-17566:
-----------------------------------
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: e4ae41fc4047c99af983020b4f33bd297c9d0ac5
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: 3h 48m agent time, 139.9M tokens, about $82 (estimate)
{noformat}
h3. Result
12 candidate findings came out of model checking (5) and code review (7), and
all 12 were investigated individually.
||Disposition||Count||
|Reproduced|5|
|Masked (defect present, harm prevented by another component today)|4|
|False positive|3|
Each finding that was filed 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-30), and the fix patch, reproduction and
report were reviewed independently before filing. Two reproduced findings
belong to open issues and are not filed again. Three masked findings have a
consequence worth fixing and are filed; one of them shares its root cause and
fix with a reproduced finding, so it is part of that issue.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17623|Major|Mis-replication of a container is not repaired while one of
its replicas is on a datanode that is DEAD in maintenance|
|HDDS-17621|Major|SCM brings a datanode back from DEAD without a full container
report, so it forgets the node's replicas for up to two hours|
|HDDS-17620|Minor|SCM sends another DELETE for an UNHEALTHY EC replica while
one is pending, and the queued copy can delete a replica later rebuilt on that
datanode|
|HDDS-17619|Minor|EC under replication handler runs over replication inline
while a reconstruction is pending and can delete one of its sources|
|HDDS-17622|Minor|RackScatter placement fails although a rack has a writable
datanode, because a new rack gets only one round of random picks|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch and a standalone reproduction test
attached. HDDS-17623 also covers the re-registration case of the same null
rack, which is masked today by the full container report sent at registration.
h3. Not filed
* Reproduced, already reported: while a replica's datanode is STALE, the EC
mis-replication handler copies a replica and the over-replication handler
deletes the copy. This is HDDS-17363 with a STALE trigger; its option 2 (count
all replicas when choosing the copy to delete) covers it, option 1 does not. At
default intervals no full loop completes, only one wasted copy per STALE
episode.
* Reproduced, already reported: after a leader change, an EC delete that
already ran on a datanode whose report is held back by a partition is repeated
on the other copy of the index by the new leader. This is the EC case of
HDDS-16449. Its proposed fix covers it only when the same SCM regains
leadership without a restart, not a failover to another SCM. The race needs
several conditions at once and has no contained fix, so it is not filed
separately.
* Masked: an UNHEALTHY EC replica is deleted while its only CLOSED twin is on a
STALE node. Within EC parity nothing changes, since reconstruction uses CLOSED
sources only; the harm beyond parity is argued, not run.
* False positive: a target shortfall caused only by overloaded datanodes
triggers the placement failure remedies. Every delete it causes removes a
replica the repair did not need.
* False positive: a pending ADD to a target that went DEAD holds repair until
the event timeout. That is the intended handling and the container is repaired
afterwards.
* False positive: excluded nodes and old term command queues survive a leader
change. The heartbeat path clears them within about one heartbeat, before the
new leader's Replication Manager acts.
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-placement-repair|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* All reproductions run real SCM code with simulated datanodes; no mini cluster
was run. The datanode side failures in HDDS-17619 and HDDS-17621 (a
reconstruction that fails when a source is deleted, or when the target already
holds the container) are argued from the datanode code, not run.
* HDDS-17621: the empty read pipeline when every holder of a container returns
from DEAD together was run; what a client then sees on an OM location cache
miss is argued from code.
* HDDS-17623 was reached through the real maintenance admin call with two state
transitions driven directly. With the fix such a container gets copies, and
with some rack orders it can then enter the loop described in HDDS-17363
(argued, not run).
* HDDS-17622 narrows the placement failure rather than removing it (in one
layout from about 76% to about 5% of attempts). Choosing only among writable
nodes, as HDDS-16634 suggests for RackAware, would remove it.
* The patches were built and tested on the pinned commit and apply to master at
3fc2387040f. The HDDS-17623 patch touches the same part of
{{SCMCommonPlacementPolicy.validateContainerPlacement}} as the open pull
request for HDDS-17381, and the HDDS-17619 test changes are near the open pull
request for HDDS-16614, so the second one to land needs a rebase.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify scm-ec-placement-repair (Apache Ozone master @e4ae41f)
> -----------------------------------------------------------------------
>
> Key: HDDS-17566
> URL: https://issues.apache.org/jira/browse/HDDS-17566
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: scm-ec-placement-repair.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-placement-repair}}. Scope and code entry points are in the attached
> guidance file [^scm-ec-placement-repair.guidance.md]. Added as a narrower
> rerun of scm-ec-replication (HDDS-16431), which modeled EC index counts at
> 9fbf9ee but abstracted placement, rack topology, node health changes and
> command throttling, and found nothing; HDDS-16623, HDDS-16629 and HDDS-14671
> have since changed dead node topology, mis replication placement and node
> states.
> h3. Run environment
> {noformat}
> Apache Ozone commit: e4ae41fc4047c99af983020b4f33bd297c9d0ac5
> 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-placement-repair|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 ({{424482e}}); 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]
