[
https://issues.apache.org/jira/browse/HDDS-17232?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18131342#comment-18131342
]
Siyao Meng commented on HDDS-17232:
-----------------------------------
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: 679c9ccbee740a0af3ca9f76fc2d4bc6586049eb
Specula: v1.2.0-34-gcdd19e39 with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 3h 58m agent time, 121.6M tokens, about $70 (estimate)
{noformat}
h3. Result
10 candidate findings came out of model checking (6) and code review (4), and
all 10 were investigated individually. Confirmation raised one spec repair
round.
||Disposition||Count||
|Reproduced|5|
|False positive|5|
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-24), and the fix patch, reproduction and
report were reviewed independently. Two of the five are already reported
upstream and one exists only with an open pull request applied, so two issues
are filed.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17425|Minor|Datanode on older software that registers while SCM finalizes
stays HEALTHY on the finalized SCM and is never asked to register again|
|HDDS-17427|Minor|Datanode restarted during SchemaV3 finalization can create a
second RocksDB for a data volume on another DB volume|
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
* Already reported: a HEALTHY datanode counts as finalized when its apparent
version equals its own software version, so the HDDS upgrade status can read
FINALIZED while a datanode on older software is in service (HDDS-16799,
reproduced at this commit).
* Already reported: a data volume that fails while the SchemaV3 finalize action
runs comes back at restart without a DB and stays in service, so container
creates on it fail. This is the HDDS-11485 defect reached through finalization;
its fix is the same as the closed apache/ozone#7240.
* Only with apache/ozone#11692 applied: an SCM that has not yet applied the
finalization asks a STALE, correctly finalized datanode to register again on
heartbeat, rejects it, and the datanode shuts down (related to HDDS-17090).
Master is not affected.
* False positive: upgrade status reads FINALIZED while a datanode that has not
finalized is not registered yet. It clears on registration and matches the
documented meaning of the status.
* False positive: SCM accepts a datanode that is not finalized at registration
after SCM finalized. This is the intended HDDS-15482 behaviour and is covered
by an existing test.
* False positive: the recorded datanode apparent version can go backwards. It
needs a report order that no real call sequence produces, and the next
heartbeat restores it.
* False positive: finalization can rewrite the datanode VERSION file without
the cluster ID. It is rewritten at container start and nothing reads it in
between.
* False positive: repeated finalize commands. They are no ops; the only effect
is a bounded delay on the datanode command thread.
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 \
"dn-upgrade-finalization|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17425 cannot be reached by any released datanode yet: releases up to
2.2.1 do not report datanode versions and are rejected at registration. It was
reproduced on the SCM side with the Ratis round trip of the finalize request
replaced by a stand in; the SCM HA route without a timing window was read from
code, not run. The patch changes what happens after {{ozone admin upgrade
finalize --force}}: HEALTHY datanodes on older software are told to register
again and shut down instead of serving until their next restart. That needs a
decision from the upgrade owners.
* HDDS-17427 needs a datanode first installed with a release before 1.3.0, two
or more DB volumes, and a stop between the SchemaV3 action and the VERSION
write followed by a retry. Harm needs a second event (the DB volume holding the
copy in use is lost or removed from the configuration); SCM counting the
resulting empty replica as healthy was argued from code, not run. Its
regression test picks DB volumes at random and passes on the unfixed code about
1 time in 729.
* The patches were built and tested on the pinned commit and apply to master at
69d77beff60. The HDDS-17425 patch also applies on top of apache/ozone#11692.
The two patches change different files.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify dn-upgrade-finalization (Apache Ozone master @679c9cc)
> -----------------------------------------------------------------------
>
> Key: HDDS-17232
> URL: https://issues.apache.org/jira/browse/HDDS-17232
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: dn-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
> {{dn-upgrade-finalization}}. Scope and code entry points are in the attached
> guidance file [^dn-upgrade-finalization.guidance.md]. Added after the Zero
> Downtime Upgrade branch (HDDS-14496) was merged. HDDS-16480 and HDDS-16549
> left datanode finalization out of scope.
> h3. Run environment
> {noformat}
> Apache Ozone commit: 679c9ccbee740a0af3ca9f76fc2d4bc6586049eb
> 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 \
> "dn-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 ({{20d95ed}}); 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]
