[
https://issues.apache.org/jira/browse/HDDS-16480?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18125927#comment-18125927
]
Siyao Meng commented on HDDS-16480:
-----------------------------------
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: a6b7bdb937109ba2893688b41a89470bc95c88cf
Specula: v1.0.0-56-g62f63a1e (with local changes)
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 40G memory, 20 workers
Total: 6h 51m agent time, 94.6M tokens, about $62 (estimate)
{noformat}
h3. Result
9 candidate findings came out of model checking (4) and code review (5), and
all 9 were investigated individually.
||Disposition||Count||
|Reproduced|3|
|Environment limited|1|
|Masked|1|
|False positive|3|
|Dropped (already reported upstream)|1|
Each reproduced and environment limited 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-10), and the fix
patch, reproduction and report were reviewed independently before filing.
h3. Filed
||Issue||Priority||Summary||
|HDDS-16860|Major|OM leader terminates on CompleteFinalizeUpgrade when a quota
repair is already running, and stays partially finalized after restart|
|HDDS-16862|Major|Finalization from a Ratis snapshot should stop at the version
recorded in the snapshot (OM, SCM)|
|HDDS-16863|Major|OM that stops during snapshot install after the DB swap
restarts pre-finalized although its DB is finalized|
|HDDS-16861|Minor|Upgrade quota repair is skipped on every OM if leadership
moves before the leader applies CompleteFinalizeUpgrade|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch attached, and all but HDDS-16862 also have
a standalone reproduction test; HDDS-16862 is covered by the regression tests
in its patch.
h3. Not filed
* The masked finding (overlapping finalize calls racing on the temporary
VERSION file) does not hold on a running OM: apply is single threaded and the
new startup call in HDDS-16863 runs before the Ratis server exists.
* The three false positives: re-running upgrade actions is the documented at
least once contract and both current actions are idempotent; a failed Ratis
submit after the SCM finalize step is retried safely; the VERSION file is
replaced atomically.
* One finding was already reported upstream, with a fix under review.
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=40G --tlc-worker-limit=20 \
"om-upgrade-finalization|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-16862 could not be run end to end, because only one OM release on the
new version framework exists. Its regression tests drive the real version
managers and version catalogs of OM and SCM.
* HDDS-16860 depends on the failed entry being flushed before the process
exits. This always happened in the mini cluster; in production it is a race.
* HDDS-16861 holds the old leader's apply with controlled timing in its
reproduction.
* HDDS-16863 and HDDS-16862 add the same
{{ComponentVersionManager.finalizeUpgrade}} helper with an identical hunk; they
merge cleanly in either order, but a plain {{git apply}} of the second patch
fails on that hunk. HDDS-16860, HDDS-16861 and HDDS-16863 change the same lines
of {{QuotaRepairUpgradeAction.execute}}, so whichever lands later needs a
trivial rebase.
* The patches were built and tested on the pinned commit and apply to master at
b0aa6475b78.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-upgrade-finalization (Apache Ozone master @a6b7bdb)
> -----------------------------------------------------------------------
>
> Key: HDDS-16480
> URL: https://issues.apache.org/jira/browse/HDDS-16480
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: om-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
> {{om-upgrade-finalization}}. Scope and code entry points are in the attached
> guidance file [^om-upgrade-finalization.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: a6b7bdb937109ba2893688b41a89470bc95c88cf
> 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-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.
> * 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]
