[
https://issues.apache.org/jira/browse/HDDS-16476?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18125739#comment-18125739
]
Siyao Meng commented on HDDS-16476:
-----------------------------------
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: 7fcf31294859d5d31163e016b5a9a63f21c6edd2
Specula: v1.0.0-56-g62f63a1e, with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 8h 42m agent time, 134.2M tokens, about $96 (estimate)
{noformat}
h3. Result
13 candidate findings came out of model checking (7) and code review (6), and
all 13 were investigated individually.
||Disposition||Count||
|Reproduced|10|
|Masked (defect present, harm prevented by another component today)|2|
|False positive|1|
Three reproduced findings share one root cause and one fix, so they are one
issue. Each issue 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-10), and the fix patch, reproduction and report were
reviewed independently before filing. Review changed three proposed fixes
(HDDS-16837, HDDS-16839, HDDS-16840). One more issue was found during that
review and is filed as well (HDDS-16842); it is not one of the 13 findings and
has no separate reproduction.
h3. Filed
||Issue||Priority||Summary||
|HDDS-16840|Major|OM bootstrap and decommission can drop other OMs or change
their Raft role|
|HDDS-16833|Major|Leader transfer reverts a concurrent OM or SCM membership
change because it rewrites the Raft configuration from a group read earlier|
|HDDS-16838|Major|OM bootstrap check passes when the new OM's own config lacks
a ring member; the OM is added as a voter and then stops with an NPE|
|HDDS-16832|Major|OM that started as a single node fails every checkpoint
install from the first OM bootstrapped onto it with a NullPointerException|
|HDDS-16839|Minor|A new OM treats any failed bootstrap reply as final and
exits, although the leader may still be adding it or may already have logged
the change|
|HDDS-16837|Minor|ozone.om.listener.nodes without the service ID suffix, as
documented, is silently ignored and the intended listener OM joins as a voter|
|HDDS-16836|Minor|ozone admin om roles reports LISTENER or FOLLOWER from the
local config of the answering OM, not from the Raft configuration|
|HDDS-16841|Minor|A repeated OM bootstrap under the other Raft role blocks
membership changes and leader transfer on the leader|
|HDDS-16842|Minor|Check admin rights in the OM bootstrap RPC handler,
consistent with decommission and getOMConfiguration|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch attached, and all but HDDS-16842 a
standalone reproduction test.
h3. Not filed
* Masked: a listener OM that is decommissioned while it is running is not
stopped. The CLI asks for the node to be stopped first, and no client failover
proxy provider contacts a listener, so nothing reads from the leftover process.
* Masked: an OM restarted after a live member was listed in
{{ozone.om.decommissioned.nodes}} starts without that member in its peer list.
The list is repaired when the next configuration entry is applied, before it is
used for a membership change.
* False positive: applying a removal for a node missing from the local peer
list is fatal while the matching add only logs. The removal candidates come
from the same list, so the fatal branch is not reachable.
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 \
"om-membership|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* All triggers are operator actions (bootstrap, decommission, leader transfer),
several of them combined with a config difference between OMs. Everything was
run on a mini cluster with the entry points behind the commands, not with the
CLI.
* HDDS-16840: the timing symptom needs a decommission inside a window of tens
of milliseconds after a bootstrap reply, and its reproduction holds that window
open. The role and forced bootstrap symptoms need no timing.
* HDDS-16833 needs two overlapping admin operations. The SCM side shares the
helper and is argued from the code, not run.
* HDDS-16832 and the first case of HDDS-16839 use the Ratis
{{CodeInjectionForTesting}} hook to stand for a partition or a slow node.
* HDDS-16839: the patch narrows the window and does not close it. The issue
names the leader side change that would.
* HDDS-16837: the patch adds a warning only. The published site page needs a
separate correction in apache/ozone-site.
* The patches were built and tested on the pinned commit and apply to master at
1cc6423590f, each on its own. HDDS-16832, HDDS-16833, HDDS-16836, HDDS-16838
and HDDS-16839 each add to {{TestAddRemoveOzoneManager}}, so after the first
one the others need a trivial rebase of that test file. Their main code changes
do not conflict. HDDS-16840 and HDDS-16841 change the same method, so the
second one to land needs a small rebase.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-membership (Apache Ozone master @7fcf312)
> -------------------------------------------------------------
>
> Key: HDDS-16476
> URL: https://issues.apache.org/jira/browse/HDDS-16476
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: om-membership.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
> {{om-membership}}. Scope and code entry points are in the attached guidance
> file [^om-membership.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: 7fcf31294859d5d31163e016b5a9a63f21c6edd2
> 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 \
> "om-membership|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]
