[
https://issues.apache.org/jira/browse/HDDS-16549?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18128121#comment-18128121
]
Siyao Meng commented on HDDS-16549:
-----------------------------------
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: 7f9b6237deb2b06d73d1ac2b78cccaa60780c3ef
Specula: v1.2.0-33-ga7646603 (with local changes)
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 2h 19m agent time, 83.3M tokens, about $51 (estimate)
{noformat}
The guidance attached to this issue names {{SCMUpgradeFinalizer}} and
{{TestScmFinalization}}, which HDDS-15379 removed. This run started from
{{FinalizationStateManagerImpl}}, {{ScmVersionManager}},
{{ComponentVersionManager}}, {{RatisBasedVersionManager}},
{{ClearFinalizingStateScmUpgradeAction}} and {{TestScmHAFinalization}}.
h3. Result
8 candidate findings came out of model checking (4) and code review (4), and
all 8 were investigated individually. No spec repair requests were raised by
confirmation.
||Disposition||Count||
|Reproduced|2|
|Masked (defect present, harm prevented by another component today)|2|
|False positive|4|
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-17), and the fix patch, reproduction and
report were reviewed independently before filing.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17089|Major|SCM that stops during snapshot install after the DB swap
restarts pre-finalized and shuts down every finalized datanode|
|HDDS-17090|Major|Follower SCM that has not applied finalization yet rejects a
datanode the leader already finalized, and the datanode shuts down|
Priorities follow the manual validation, not the pipeline's severity classes
(both were classed Critical). Each issue has a proposed fix patch and a
standalone reproduction test attached.
h3. Not filed
* Masked: an SCM that crashes after applying FINALIZE and before its
transaction buffer is flushed skips the upgrade action on replay, because the
VERSION file is already finalized. The only action whose effect is lost removes
the leftover pre ZDU {{#FINALIZING}} key, which nothing reads.
* Masked: an upgrade action run during snapshot install writes into the
transaction buffer that {{SCMStateMachine.reinitialize}} then discards. The
lost write is the same unread key, and the leader's checkpoint already carries
the correct state.
* False positive: the FINALIZE entry carries no target version, so replicas
with different software could finalize to different versions. No second version
after ZDU exists at this commit; the snapshot part is HDDS-16862.
* False positive: an upgrade action that fails on every replay stops every SCM
on every restart. Stopping on a failed action is intended, and no shipped
action can fail that way.
* False positive: the peer version check before finalize uses the configured
peer list and can race a peer restart. It is documented as a best effort guard,
and mixed software during finalization is out of scope.
* False positive: finalize is accepted in safe mode and the datanode check
passes with no registered datanodes. Treated as operator error by the design;
noted as possible hardening.
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-upgrade-finalization|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17089 needs {{ozone.scm.ha.ratis.log.purge.enabled=true}} (default
false) so that an existing SCM installs a snapshot, plus a process kill between
the DB swap and the VERSION write (77 ms in the test run, longer with many
containers to reload). The reproduction places the kill with a test upgrade
action and restarts from a copy of the metadata directory; no real process kill
was run. Its patch shares two framework hunks with the HDDS-16863 patch; they
merge cleanly in either order.
* HDDS-17090 needs a follower SCM that stays behind the leader (partitioned
from it or stalled, but reachable by datanodes) across the leader finalizing
the datanodes and a datanode restart. Ordinary apply lag of milliseconds does
not trigger it; the reproduction cuts the follower off with the existing Ratis
{{CodeInjectionForTesting}} hook. The checkpoint install variant was argued
from code, not run. The patch also changes two other outcomes, described in the
issue: a rejection from an SCM that is not the ready leader is no longer final
for any reason.
* The patches were built and tested on the pinned commit and apply to master at
268654683b4.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify scm-upgrade-finalization (Apache Ozone master @7f9b623)
> ------------------------------------------------------------------------
>
> Key: HDDS-16549
> URL: https://issues.apache.org/jira/browse/HDDS-16549
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: scm-upgrade-finalization.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-upgrade-finalization}}. Scope and code entry points are in the attached
> guidance file [^scm-upgrade-finalization.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: 7f9b6237deb2b06d73d1ac2b78cccaa60780c3ef
> 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-upgrade-finalization|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.
> * The two entry points named in the attached guidance file
> ({{SCMUpgradeFinalizer}}, {{TestScmFinalization}}) were removed by
> HDDS-15379. This run starts from {{FinalizationStateManagerImpl}},
> {{ScmVersionManager}}, {{ComponentVersionManager}} and
> {{TestScmHAFinalization}} instead.
> * 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]
