[
https://issues.apache.org/jira/browse/HDDS-17429?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18131918#comment-18131918
]
Siyao Meng commented on HDDS-17429:
-----------------------------------
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: a5814528cdc8d3c1b27f259e0db2256b585cb825
Specula: v1.2.0 (f5285a2b), with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: about 2h 17m agent time, 83.9M tokens, about $52 (estimate)
{noformat}
h3. Result
13 candidate findings came out of model checking (3) and code review (10), and
all 13 were investigated individually.
||Disposition||Count||
|Reproduced|5|
|False positive|7|
|Dropped (duplicate of an existing report)|1|
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-25), and the fix patch, reproduction and
report were reviewed independently before filing. One reproduced finding needs
two independent fixes and is filed as two issues. Two further defects were
found during that validation and review, in the same code area, and are filed
as well.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17468|Critical|Rename responses miss an earlier snapshotRenamedTable put
in the same flush batch, so blocks a snapshot still holds can be reclaimed|
|HDDS-17469|Critical|OMKeysRenameResponse writes renames whose sources and
destinations overlap in map order, so the committed key table differs from the
cache (found during validation)|
|HDDS-17458|Major|DeleteBucket after the purge of the bucket's last snapshot
succeeds or fails depending on the OM's flush timing, so OM replicas diverge|
|HDDS-17459|Major|OM restart re-creates a deleted S3 volume outside Ratis and
replaces the OM user's volume list, so OMs diverge|
|HDDS-17467|Major|snapshotRenamedTable entry moved into the active DB from a
deleted snapshot is overwritten by a rename response flushed in the same batch
(found during review)|
|HDDS-17457|Minor|Bucket creation right after a bucket delete is rejected with
TOO_MANY_BUCKETS at the bucket limit, because the deleted bucket is still
counted|
|HDDS-17460|Minor|Table cache cleanup executors are never shut down, so OM
checkpoint installs and Recon OM DB syncs leak threads and keep old caches in
memory|
|HDDS-17461|Minor|After a checkpoint install, OM volume, bucket and snapshot
directory metrics keep reading the replaced metadata manager|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch attached. HDDS-17468 and HDDS-17469 carry
the patch only, with their regression tests as the reproduction; the others
also have a standalone reproduction test.
h3. Not filed
* Dropped: the volume and user table cache entries that OMTenantCreateRequest
leaves after TENANT_ALREADY_EXISTS are already reported as HDDS-17197.
* False positive: table cache state could disagree with the DB across flush,
eviction, pause, checkpoint install and restart. Epoch exact eviction,
monotonic indices, the flush pause and fresh caches on reload kept them
consistent in every path tested.
* False positive: the startup S3 volume user entry is cached with an epoch that
is never evicted. It is one entry that does not grow and never shadows a DB
value.
* False positive: TableCacheUpdateTracker.close leaves its ThreadLocal set when
the body throws. The next track() overwrites it and the stale value is never
read.
* False positive: handleWriteRequest skips the double buffer for Prepare. That
branch is unreachable at this commit.
* False positive: OMBucketDeleteRequest adds the bucket delete marker before
the VOLUME_NOT_FOUND check. An earlier check fails first, and the state cannot
be reached through requests.
* False positive: cleanupCache resolves table names that might not belong to
the active DB. Every table name a real request records resolves.
* False positive: OMSnapshotMoveDeletedKeysResponse reads a table while adding
to the batch. It reads an already committed snapshot DB, so the result does not
depend on batch boundaries.
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-table-cache-cleanup|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17468, HDDS-17467 and HDDS-17458 depend on which transactions one double
buffer flush commits together. Their tests hold the flush with the existing
{{OzoneManagerDoubleBuffer}} pause hook. Without the hook, 64 keys renamed
twice from 8 threads on one OM gave no case for HDDS-17468 (pipeline run). An
OM that applies a backlog, such as a follower catching up or an OM replaying
its log, flushes consecutive transactions together (argued, not run).
* HDDS-17458 was reproduced on two in process replicas, not on an OM HA ring.
Its patch waits for the double buffer flush inside apply, which holds the apply
thread for that time.
* HDDS-17469 changes behaviour: a request whose pairs share a key name is now
rejected as a whole with INVALID_REQUEST.
* Block deletion on datanodes was not run for the issues that send blocks to
SCM; the tests record the blocks sent for deletion.
* The patches were built and tested on the pinned commit and apply to master at
88119243f99. HDDS-17459 and HDDS-17461 touch the same test imports, so the
second one to land needs a trivial rebase. HDDS-17458 conflicts textually with
open pull request apache/ozone#10965 (HDDS-16060) in the same method.
HDDS-17460 and HDDS-17461 are independent and apply together.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-table-cache-cleanup (Apache Ozone master @a581452)
> ----------------------------------------------------------------------
>
> Key: HDDS-17429
> URL: https://issues.apache.org/jira/browse/HDDS-17429
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: om-table-cache-cleanup.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-table-cache-cleanup}}. Scope and code entry points are in the attached
> guidance file [^om-table-cache-cleanup.guidance.md]. Added after HDDS-13365
> and HDDS-16643 replaced per-response cleanup lists with automatic cache
> tracking. HDDS-16427 covered the double buffer before this change, and later
> runs checked cleanup for single tables only (HDDS-16567, HDDS-17230).
> h3. Run environment
> {noformat}
> Apache Ozone commit: a5814528cdc8d3c1b27f259e0db2256b585cb825
> 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-table-cache-cleanup|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 ({{69d77be}}); 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]
