[
https://issues.apache.org/jira/browse/HDDS-16468?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18122161#comment-18122161
]
Siyao Meng commented on HDDS-16468:
-----------------------------------
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, and
severity classification.
h3. Run environment
{noformat}
Ozone commit: 20e6a1c0f6039248373efd3eb1d7f2afcf7f1535
Specula: v1.2.0
Agent/model: claude-code, Claude Opus 5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Runtime/cost: 6h 47m, 132.4M tokens, about $108
{noformat}
h3. Result
19 candidate findings were consolidated from model checking (MC-1..MC-6) and
code review (T1..T6, R1..R15), then investigated individually.
||Disposition||Count||
|Reproduced|11|
|Env limited|1|
|Masked (latent, no production caller today)|4|
|False positive|3|
Severity of the 12 findings filed: 3 Critical, 6 Major and 3 Minor.
h3. Patches
Eight of the twelve carry a patch against
20e6a1c0f6039248373efd3eb1d7f2afcf7f1535, attached to the individual issues.
Seven of those include a regression test that was verified to fail without the
fix and pass with it: MC-2, MC-3, CR-R6, CR-R11, CR-R13, CR-T1 and CR-R12.
CR-R14 is fix only, because its test fixture needs Mockito's inline mock maker,
which the verification host cannot run.
Four are filed as analysis only, with no patch: MC-1, MC-4, MC-5 and CR-MC5.
Each of those needs a semantic decision rather than a correction, for example
whether invalidate() may leave an entry in the cache, where the deletion
services release their snapshot handles, and whether a first time snapshot load
may happen twice concurrently. The approach is worth agreeing before a patch is
written, and a regression test for the two deadlocks would be slow and timing
dependent in CI.
h3. Bugs filed
All twelve are linked to this issue with the Testing link type.
* HDDS-16684 (Critical) Deletion services hold SNAPSHOT_DB_LOCK stripe read
locks across a synchronous Ratis submit, deadlocking against the double buffer
flush thread applying a snapshot purge. Whole OM commit path parks, untimed,
restart only. [MC-4]
* HDDS-16685 (Critical) Nested snapshot {{get()}} takes stripes in caller order
and inverts against the checkpoint's ascending {{acquireAll}}, deadlocking
snapdiff against checkpoint or follower bootstrap. [MC-5]
* HDDS-16686 (Critical) The eviction pass removes the key from
{{pendingEvictionQueue}} on every branch, so a concurrent release is erased and
an unreferenced snapshot DB stays open and unqueued forever; every later
checkpoint then fails the cache drain check. [MC-2]
* HDDS-16687 (Major) {{SnapshotCache.invalidate}} closes the snapshot RocksDB
with no refcount check and no lock, so a purge closes a DB under a live reader
and the reader's handle fails permanently. [MC-1]
* HDDS-16688 (Major) The checkpoint servlet transfers snapshot SST files before
taking {{snapshotCache.lock()}}, so a purge during that window aborts the whole
checkpoint with NoSuchFileException. [MC-3]
* HDDS-16689 (Major) A first time snapshot {{get}} runs the HDDS-13633 flush
poll inside the ConcurrentHashMap bin lock that purge time {{invalidate}}
needs, stalling the double buffer and every OM write for the poll timeout (20s
default). [CR-MC5]
* HDDS-16690 (Major) An unbalanced {{MultiSnapshotLocks.releaseLock()}} from
{{ReclaimableFilter}} drives the DAG per thread counter negative and silently
disables the lock order check on pooled deletion service threads. [CR-R6]
* HDDS-16691 (Major) A retriable snapshot load TIMEOUT is rewrapped as an
unchecked IllegalStateException, so clients get an unstructured RemoteException
instead of status TIMEOUT and lose the retry hint. [CR-R11]
* HDDS-16692 (Major, env limited) {{OMSnapshotMoveDeletedKeysResponse}} writes
both snapshots' tables without SNAPSHOT_DB_CONTENT_LOCK, unlike its sibling
response. [CR-R14]
* HDDS-16693 (Minor) Nested snapshot read locks on two stripes of one resource
feed a bogus elapsed time into the OM read lock hold time statistic. [CR-R13]
* HDDS-16694 (Minor) A failed snapshot load still increments
{{NumSnapshotCacheSize}}, so the gauge drifts upward monotonically. [CR-T1]
* HDDS-16695 (Minor) {{RDBStore.close()}} unregisters the process wide RocksDB
metrics source shared with the active OM DB, so routine snapshot eviction
resets JMX counters to zero. [CR-R12]
h3. Latent findings, not filed
Four findings are real code defects with no production trigger today, so they
are recorded but not filed as bugs: {{release(UUID)}} and cross thread
{{close()}} stranding a handle and its stripe read hold [MC-6], an unguarded
{{scheduleWithFixedDelay}} eviction pass whose first escaping throwable
silently ends all eviction [CR-R2], a narrow {{catch (IOException)}} in the
snapshot metadata manager constructor that can leak an open RocksDB and its
LOCK file [CR-R10], and the context free drain failure message [CR-R9]. Say the
word if these should be filed as hardening issues.
h3. Reproduce
{code:none}
specula run --agent=claude-code --effort=medium --model='claude-opus-5[1m]' \
--max-parallel=2 --enable-reviews --legacy-confirm \
--tlc-memory-limit=28G --tlc-worker-limit=8 \
"om-snapshot-cache|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* Confirmation ran in legacy single agent mode rather than the campaign default
of parallel per finding confirmation with the adversarial Challenger debate,
because the parallel dispatcher creates a git backed trusted working directory
that this host denied. Confirmation is therefore less adversarial than in
earlier targets in this umbrella.
* MC-2 did not trigger in 4000 unassisted iterations: the race window between
the refcount read and the queue removal is a single debug log statement. It was
reproduced by widening that window with an instrumentation patch, so the
ordering is real and the consequence is demonstrated, but the natural
probability is low.
* CR-R14 is env limited: this host has no Ozone cluster and no pre upgrade Raft
log, so the upgrade replay trigger could not be produced. The filing rests on
the verified source asymmetry against its sibling response.
* Model checking and trace validation were run against 5 collected trace
scenarios covering checkpoint versus get, close guard release, eviction versus
reference, purge versus reader, and slow load timeout.
Generated with Specula (Claude Opus 5).
> [Specula] Verify om-snapshot-cache (Apache Ozone master @20e6a1c)
> -----------------------------------------------------------------
>
> Key: HDDS-16468
> URL: https://issues.apache.org/jira/browse/HDDS-16468
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: om-snapshot-cache.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-cache}}. Scope and code entry points are in the attached
> guidance file [^om-snapshot-cache.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: 20e6a1c0f6039248373efd3eb1d7f2afcf7f1535
> 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-cache|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
> * 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]
