[
https://issues.apache.org/jira/browse/HDDS-16537?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18126181#comment-18126181
]
Siyao Meng commented on HDDS-16537:
-----------------------------------
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: b0aa6475b7856d2c7f467dd3db12b9a1dd116f63
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: 8h 37m agent time, 166.1M tokens, about $105 (estimate)
{noformat}
h3. Result
17 candidate findings came out of model checking (9) and code review (8), and
all 17 were investigated individually.
||Disposition||Count||
|Reproduced|10|
|Masked (defect present, harm prevented by another component today)|4|
|False positive|3|
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-11), and the fix patch, reproduction and
report were reviewed independently before filing.
h3. Filed
||Issue||Priority||Summary||
|HDDS-16928|Major|SCM never catches up after a checkpoint install that fails or
is interrupted once Ratis has acknowledged it, even after a restart|
|HDDS-16925|Major|SCM forgets all container replicas when it installs a Ratis
snapshot, until the next full container reports|
|HDDS-16924|Major|SCM that installed a Ratis snapshot in process keeps serving
checkpoints from the closed DB, so downloads from it fail once it is leader|
|HDDS-16923|Major|SCM snapshot install replaces scm.db before saving the
leader's secret keys, so a failure in between later drops unexpired secret keys
on all SCMs|
|HDDS-16930|Major|Follower SCM exits when it installs a Ratis snapshot after
applying a delete transaction removal that its buffer has not flushed yet|
|HDDS-16931|Minor|SCM checks only the TransactionInfo of a downloaded
checkpoint before acknowledging it, so a checkpoint with corrupt SST blocks is
installed|
|HDDS-16932|Minor|SCM follower rejects every append from a new leader when
leadership moves while it downloads a checkpoint that then succeeds|
|HDDS-16929|Minor|SCM follower stops applying the Raft log, while reporting
RUNNING, if the transaction buffer init fails after a checkpoint install|
|HDDS-16927|Minor|SCM never deletes the checkpoint it downloads for a Ratis
snapshot install, leaving a full DB copy in its snapshot directory per install|
|HDDS-16922|Minor|SCM terminates with exit status 0 when it shuts itself down
on a fatal error, such as a failed Ratis snapshot install|
|HDDS-16921|Minor|SCM checkpoint install rollback restores the old DB without
closing the open checkpoint DB, so it reloads the rejected checkpoint|
|HDDS-16920|Minor|SCM creates the DB inconsistent marker only after moving
scm.db away, so a stop in between restarts on an empty DB|
|HDDS-16919|Minor|SCMSnapshotProvider sets the thread interrupt flag when the
checkpoint download fails without an interrupt|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch and a standalone reproduction test
attached, with two exceptions: HDDS-16928 has a test only patch and a
recommended design, because the fix needs a design decision, and HDDS-16932 has
no patch or attachment. The four masked findings are filed (HDDS-16925,
HDDS-16921, HDDS-16920, HDDS-16919) because the fixes are small; manual
validation found HDDS-16925 is protected only by timing.
h3. Not filed separately
* Reproduced: after a snapshot install, the datanode to pipeline map keeps
deleted pipelines. It was found independently by the pipeline lifecycle run and
is filed as HDDS-16905.
* Reproduced: a pending install is never consumed after a leader change when
the checkpoint download fails because the leader stops. The patch attached to
HDDS-16899 fixes this case; the case it does not cover is HDDS-16932.
* The three false positives were judged not to hold on a running SCM: designed
handling before same thread termination, index checks that agree on every
reachable input, and a guard that behaves correctly.
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 \
"scm-checkpoint-install|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* A running follower installs a checkpoint only with
{{ozone.scm.ha.ratis.log.purge.enabled}} on, which is off by default, or when
an SCM is added with {{--bootstrap}}. HDDS-16925, HDDS-16930, HDDS-16929 and
HDDS-16932 need the former; HDDS-16928 and HDDS-16924 also happen on bootstrap
at default settings.
* HDDS-16928, HDDS-16923, HDDS-16931 and HDDS-16920 need a fault or a stop
inside a short window of the install. Disk faults, injected failures and, for
HDDS-16931, a process kill were run; the other kill and power loss variants
were argued from code. The cluster wide outage in HDDS-16928 was shown only
through an admin leadership transfer.
* HDDS-16925: the consequences on a leader with the wiped view (MISSING
marking, replication then excess deletion, EC decommission counted finished)
were shown with the real check handlers, not through a failover and the
decommission monitor.
* HDDS-16930: a restart right after the failed install also failed in a review
run (the restored DB would not open); with the HDDS-16921 patch the same
restart succeeded.
* Several patches touch the same install methods and tests. HDDS-16923 and
HDDS-16929 conflict in {{SCMStateMachine}} and its test; HDDS-16924 and
HDDS-16927 both append to {{TestSCMInstallSnapshot.testInstallCheckPoint}};
HDDS-16930 and HDDS-16921 share test imports. The second of each pair to land
needs a rebase. The regression tests of HDDS-16930 and HDDS-16921 sit in
{{TestSCMInstallSnapshotWithHA}}, which does not run in regular CI.
* The patches were built and tested on the pinned commit and apply to master at
52812559dad.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify scm-checkpoint-install (Apache Ozone master @b0aa647)
> ----------------------------------------------------------------------
>
> Key: HDDS-16537
> URL: https://issues.apache.org/jira/browse/HDDS-16537
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: scm-checkpoint-install.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-checkpoint-install}}. Scope and code entry points are in the attached
> guidance file [^scm-checkpoint-install.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: b0aa6475b7856d2c7f467dd3db12b9a1dd116f63
> 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-checkpoint-install|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]
