[
https://issues.apache.org/jira/browse/HDDS-16574?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18130172#comment-18130172
]
Siyao Meng commented on HDDS-16574:
-----------------------------------
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
Challenger debate, one round of spec repair, and severity classification.
h3. Run environment
{noformat}
Ozone commit: e0de543cbe9d73f3bf5473a45e1c59cd6eae7173
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: 3h 53m agent time, 164.3M tokens, about $101 (estimate)
{noformat}
h3. Result
16 candidate findings came out of model checking (8) and code review (8), and
all 16 were investigated individually. One model checking counterexample led to
a spec repair request; after the repair it was judged a false positive.
||Disposition||Count||
|Reproduced|7|
|Masked (defect present, harm currently covered elsewhere)|3|
|False positive|4|
|Dropped as already reported|2|
The reproduced findings and one masked finding were 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-21), and the fix patch and
report were reviewed independently before filing.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17292|Critical|OMKeyRequest takes a second BUCKET lock while holding one,
out of stripe order, which can deadlock the OM apply thread|
|HDDS-17291|Major|SST value pruner waits for the bootstrap lock while holding
the differ monitor, so OM bootstrap can deadlock with snapshot diff or defrag|
|HDDS-17293|Major|OM double buffer flush of SnapshotMoveTableKeys can deadlock
with the DB checkpoint servlet on snapshot DB lock stripes, stopping all OM
writes|
|HDDS-17296|Minor|After an OM installs a checkpoint, reconfiguring the
directory deleting interval restarts the replaced DirectoryDeletingService as
well|
|HDDS-17297|Minor|Reconfiguring the SST filtering interval while an OM installs
a checkpoint starts an SstFilteringService on the replaced KeyManager|
|HDDS-17295|Minor|OzoneManager read paths release their volume or bucket read
lock on a lock that a checkpoint install may have replaced|
Priorities follow the manual validation, not the pipeline's severity classes.
Every issue has a proposed fix patch with regression tests; all except
HDDS-17292 also have a standalone reproduction test. HDDS-17291 covers two
reproduced findings with the same cause (one with snapshot diff, one with
snapshot defrag). HDDS-17295 is a masked finding that is filed because
validation showed a failed read on a follower during an install.
h3. Not filed
* Reproduced, already reported: the cycle of SnapshotDefragService,
DirectoryDeletingService, the Ratis apply and the double buffer flush is the
defect of HDDS-16164 and HDDS-16684. With the patch of apache/ozone#11009
applied, its reproduction completes.
* Masked: the lock order tracker clears a level on any release, so an inverted
BUCKET then VOLUME acquisition goes unchecked; all such write locks are taken
on the single apply thread today.
* Masked: PoolBasedHierarchicalResourceLockManager borrows from a blocking pool
inside ConcurrentHashMap.compute; it deadlocks only when the pool runs dry,
which needs ozone.om.hierarchical.resource.locks.hard.limit far below its
default.
* Dropped as already reported: duplicates of HDDS-16690 and HDDS-16858.
* False positives: a defrag task outliving install (the counterexample step
cannot happen in the code, and the spec was repaired), an unwound OBS key path
lock, the unbounded wait in OzoneManagerStateMachine.pause, and reconfiguration
callbacks run under the reconfiguration lock.
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-lock-order|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17291 needs the native rocks-tools library, which does not load on RHEL
or Rocky Linux 9 in 2.2.1 (HDDS-17153). Its reproductions use the real locks,
DB and differ, but mock the native SST reader and replay the checkpoint
servlet, snapshot diff and defrag at their lock calls. The defrag case also
needs defrag enabled and a non default bootstrap lock stripe count.
* HDDS-17293 needs a SnapshotMoveTableKeys batch applied just before a follower
bootstrap takes the bootstrap write lock, whose flush is still running when the
servlet locks the snapshot cache.
* HDDS-17292 has no standalone reproduction; its regression test sets up the
two conflicting lock holders through internal calls.
* For HDDS-17296 the restart of the replaced service was shown; the double
purge and the negative bucket usage that can follow were argued, not run.
* The patches were built and tested on the pinned commit and apply to master at
2cd413d168d (the HDDS-17292 patch with git apply -3, because HDDS-17162 changed
its test imports). HDDS-17297 and HDDS-17295 add tests at the same place in
TestOMRatisSnapshots, so whichever lands second needs a trivial rebase.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-lock-order (Apache Ozone master @e0de543)
> -------------------------------------------------------------
>
> Key: HDDS-16574
> URL: https://issues.apache.org/jira/browse/HDDS-16574
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: om-lock-order.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-lock-order}}. Scope and code entry points are in the attached guidance
> file [^om-lock-order.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: e0de543cbe9d73f3bf5473a45e1c59cd6eae7173
> 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-lock-order|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]
