[
https://issues.apache.org/jira/browse/HDDS-17552?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18134874#comment-18134874
]
Siyao Meng commented on HDDS-17552:
-----------------------------------
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: 284fad307bfd129fca3f4966d854ac45ea3b0d11
Specula: v1.2.0-35-gf5285a2b (with local changes)
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 3h 39m agent time, 87.6M tokens, about $57 (estimate)
{noformat}
h3. Result
11 candidate findings came out of model checking (3) and code review (8), and
all 11 were investigated individually.
||Disposition||Count||
|Reproduced|4|
|False positive|6|
|Dropped (already reported)|1|
Two reproduced findings share 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-30), and the fix patch, reproduction and report were reviewed
independently before filing.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17604|Major|A duplicate snapshot purge removes a new ACTIVE snapshot that
was created with the purged snapshot's name|
|HDDS-17603|Major|OM persists the index of a write that fails with
INTERNAL_ERROR before it terminates, so after restart it never applies that
write|
|HDDS-17605|Minor|Deleting services can mark the wrong snapshot deep cleaned
after a snapshot rename, or undo the deep clean reset of a snapshot purge|
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
* Dropped: a corrupted snapshot chain makes every chain touching request fail
and terminate the OM. Already reported as HDDS-9745 and HDDS-10524.
* False positive: the chain rebuilt from the flushed table plus replay always
equals the in memory chain.
* False positive: colliding snapshot IDs. No reachable path to a collision was
found.
* False positive: unsynchronized reads of the latest and oldest global snapshot
IDs from service threads. Every such read is validated again on the apply
thread.
* False positive: the purge response deletes the checkpoint directory and
invalidates caches before the batch commits. A snapshot purge is always flushed
in a batch of its own.
* False positive: snapshot rename and set property do not stamp the last
transaction info. No reader sees a wrong result from it.
* False positive: loading the chain catches only {{IOException}}. Every corrupt
table state seen surfaces as an {{IOException}} and marks the chain corrupted.
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-snapshot-chain|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17604 needs a leader change while the first purge is committed but not
yet applied on the new leader, a snapshot deleting service run in that window,
and a create with the same name between the two purges. The leader readiness
gap it relies on is HDDS-17579. The duplicate purge itself was supplied by the
test and not run on a multi OM cluster.
* HDDS-17603 needs a fault local to one OM (a read error during a snapshot
purge, or a snapshot chain marked corrupted on load). It extends the mechanism
of HDDS-16860 beyond that issue's trigger. With the patch, an error that is
deterministic on every OM makes every OM fail again on replay until the cause
is fixed; the issue describes this and the recovery.
* HDDS-17605 covers two findings with one fix. The rename case needs
{{ozone.om.snapshot.rename.allowed=true}} (default false) from 2.2.0, and both
cases need snapshot deep cleaning, which is on by default only from 2.2.0. The
harm is deleted keys or directories that are not reclaimed until a related
snapshot is purged. The patch rechecks the snapshot before the flag is sent, so
it narrows both races without closing them; a check at apply time would need a
new request field behind a layout feature. It relates to HDDS-16464, which
covers the key flag variant of the purge case.
* The patches were built and tested on the pinned commit and apply to master at
6135e81a09a.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-snapshot-chain (Apache Ozone master @284fad3)
> -----------------------------------------------------------------
>
> Key: HDDS-17552
> URL: https://issues.apache.org/jira/browse/HDDS-17552
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: om-snapshot-chain.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-snapshot-chain}}. Scope and code entry points are in the attached
> guidance file [^om-snapshot-chain.guidance.md]. Added because HDDS-15928
> checked the snapshot chain with a hand written TLA+ model, not with Specula
> against the code, and HDDS-17270 has since changed how a failed snapshot
> purge is handled.
> h3. Run environment
> {noformat}
> Apache Ozone commit: 284fad307bfd129fca3f4966d854ac45ea3b0d11
> 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-snapshot-chain|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 ({{74863e3}}); 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]
