[ 
https://issues.apache.org/jira/browse/HDDS-16576?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18130622#comment-18130622
 ] 

Siyao Meng commented on HDDS-16576:
-----------------------------------

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: bf3829e6c8ac69ae17585585703f91426dcdf6b3
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:        2h 5m agent time, 91.0M tokens, about $58 (estimate)
{noformat}

h3. Result
15 candidate findings came out of model checking (3) and code review (12), and 
all 15 were investigated individually. Trace validation converged in its first 
round, and no spec repair requests were raised by confirmation.

||Disposition||Count||
|Reproduced|5|
|Masked (defect present, harm prevented by another component today)|1|
|False positive|6|
|Already reported|3|

Each reproduced finding is its own issue with its own fix. 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-22), and the fix patch, reproduction and report were reviewed 
independently before filing.

h3. Filed
||Issue||Priority||Summary||
|HDDS-17358|Major|Closing the OM DB during a compaction DAG prune batch stalls 
for 60 seconds and can then crash the OM when the pruner reads the freed DB|
|HDDS-17355|Major|Datanode stop aborts halfway when a schema V1/V2 container DB 
is still in use, ContainerCache.shutdownCache throws IllegalArgumentException|
|HDDS-17359|Minor|OmSnapshotManager.close frees the snapshot diff DB while a 
snapshot diff job that outlived the 60 second wait still uses it|
|HDDS-17354|Minor|Interrupted RocksDatabase close frees the native DB while an 
iterator still holds it, crashing the JVM on the next iterator call|
|HDDS-17356|Minor|Data scan marks a container UNHEALTHY when its DB reopen 
fails on the lock still held after a RocksDB error close|

Priorities follow the manual validation, not the pipeline's severity classes 
(Critical for HDDS-17358 and HDDS-17359, High for the other three). Each issue 
has a proposed fix patch and a standalone reproduction test attached.

h3. Not filed
* Masked: a schema V1/V2 container export race that overlaps the open 
HDDS-11721. Exports fail loudly and are retried, and no incoherent replica was 
accepted. Not filed separately.
* False positive (6): a column family drop that the production drop sequence 
makes safe, a claimed native leak on failed open (a failed open releases the DB 
and its LOCK), a null checkpoint return that every caller handles like the 
declared exception, a lost race in {{DatanodeStoreCache.addDB}} that the 
RocksDB LOCK rules out, a double iterator close reachable only from a test, and 
repeated or concurrent {{RDBStore.close}} calls, which cause no exception, hang 
or loss.
* Already reported (3): the differ compaction listener locking on itself 
(HDDS-17259), the schema V3 store cache serving a DB that closed itself on 
error (HDDS-13994), and {{getUpdatesSince}} releasing its DB reference before 
returning the WAL iterator (HDDS-14856).

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 \
  "rocksdb-handle-lifecycle|apache/ozone|Java|Use the target-specific guidance"
{code}

h3. Caveats
* HDDS-17358 crashes only if the prune batch still has entries when the DB is 
freed; with a small batch the pruner finishes on a live DB. The reproduction 
uses a large compaction log backlog, and it stubs the check for the rocks tools 
native library, which is not built on the test host (the path under test does 
not call it). The 60 second stall on close is seen whenever a batch is running.
* HDDS-17359 needs a snapshot diff job in a long step that outlives the 60 
second wait. The reproduction holds the job with a blocking mock inside the 
real job. With the patch a follower installing a checkpoint exits through its 
error path instead of crashing (argued from the code, not run). HDDS-14856 
(reference counting for raw DB users) is the broader fix.
* HDDS-17354 needs a close on a thread that gets interrupted. The only sources 
found are in stop paths (a shutdown hook that times out and is cancelled), so 
the crash replaces an exit that was already happening. The reproduction 
interrupts the closer the way {{ShutdownHookManager}} does.
* HDDS-17355 and HDDS-17356 affect schema V1/V2 container DBs only. HDDS-17356 
needs a RocksDB Corruption or IOError while an iterator is open, which the 
reproduction creates by corrupting SST files; client requests in the window 
still fail until the old instance is freed.
* The patches were built and tested on the pinned commit and apply to master at 
fa3c98f189e. They are independent of each other. HDDS-17358 touches the same 
loop as the patch on HDDS-17291, and HDDS-17356 changes lines next to the open 
pull request for HDDS-17261, so the second to land in each pair needs a small 
rebase.
* The patches are proposals for review.

Generated with Specula (Claude Opus 5.5).

> [Specula] Verify rocksdb-handle-lifecycle (Apache Ozone master @bf3829e)
> ------------------------------------------------------------------------
>
>                 Key: HDDS-16576
>                 URL: https://issues.apache.org/jira/browse/HDDS-16576
>             Project: Apache Ozone
>          Issue Type: Sub-task
>            Reporter: Siyao Meng
>            Assignee: Siyao Meng
>            Priority: Minor
>              Labels: specula
>         Attachments: rocksdb-handle-lifecycle.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
> {{rocksdb-handle-lifecycle}}. Scope and code entry points are in the attached 
> guidance file [^rocksdb-handle-lifecycle.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: bf3829e6c8ac69ae17585585703f91426dcdf6b3
> 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 \
>   "rocksdb-handle-lifecycle|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
(v10.3.26#10030026)

---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]

Reply via email to