[
https://issues.apache.org/jira/browse/HDDS-16477?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18125956#comment-18125956
]
Siyao Meng commented on HDDS-16477:
-----------------------------------
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: 13h 19m agent time, 215.0M tokens, about $137 (estimate)
{noformat}
h3. Result
22 candidate findings came out of model checking (8) and code review (14), and
all 22 were investigated individually.
||Disposition||Count||
|Reproduced|5|
|Masked (defect present, harm prevented by another component today)|2|
|False positive|11|
|Dropped (already reported upstream)|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-11), and the fix patch, reproduction and
report were reviewed independently before filing. Manual validation of the
Recon checkpoint fetch path found two further bugs, filed the same way
(HDDS-16880, HDDS-16882).
h3. Filed
||Issue||Priority||Summary||
|HDDS-16865|Major|OM deletes its pre-install DB backup before the installed
Ratis checkpoint is synced, so a power loss can leave om.db unopenable|
|HDDS-16878|Major|OM checkpoint servlets keep using the DB store closed by a
checkpoint install and return HTTP 500 once that OM is leader|
|HDDS-16879|Minor|RevokedSTSTokenCleanupService keeps the metadata manager
closed by a checkpoint install, so every cleanup run fails while that OM is
leader|
|HDDS-16864|Minor|OM follower leaves the downloaded checkpoint tarball in the
ratis snapshot dir when untar fails|
|HDDS-16880|Minor|Recon reuses the truncated file left by a failed OM DB
checkpoint untar, so its retry from the same OM leader builds a DB with a
truncated SST|
|HDDS-16882|Minor|Recon swallows the RocksDB open failure of a fetched OM DB
snapshot, logs success and keeps using its deleted previous OM DB|
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
* One reproduced finding (an applied but unflushed write lost when a failed
install rolls back) is HDDS-16275, with a fix under review in
apache/ozone#11190. A reproduction and a note on the remaining case were added
to that PR.
* The two masked findings were reached only through a simulated crash or
injected unchecked exceptions, and the state is repaired today (the leader
resyncs the follower, or the candidate dir is wiped after the next install).
* The eleven false positives were judged not to hold on a running OM: invariant
artifacts of the model, unreachable orderings, or intended behaviour.
* Four findings were already reported upstream.
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-checkpoint-install|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-16865 was reproduced with a block level power cut in 6 of the 8 runs
that reached the cut; a full OM was not booted on the damaged directory, the
open failure follows from the shared RocksDB open path.
* HDDS-16864 was reproduced with a leader response cut off mid stream; that the
leaked tarballs exhaust a real disk is argued, not run. HDDS-16880 needs an
untar that fails after a complete download (a truncated archive served with
HTTP 200, or a full disk during the untar); neither was run on a real cluster.
* HDDS-16878 orders the first servlet request before the install with an
existing test hook.
* The HDDS-16865 and HDDS-16864 patches conflict with apache/ozone#11086 and
#11214 only in test files; the main code applies. HDDS-16880 conflicts with
#11468 only in test files. HDDS-16880 and HDDS-16882 apply in either order.
* The patches were built and tested on the pinned commit and apply to master at
6818707698c.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-checkpoint-install (Apache Ozone master @a6b7bdb)
> ---------------------------------------------------------------------
>
> Key: HDDS-16477
> URL: https://issues.apache.org/jira/browse/HDDS-16477
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: om-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
> {{om-checkpoint-install}}. Scope and code entry points are in the attached
> guidance file [^om-checkpoint-install.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-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]
