[
https://issues.apache.org/jira/browse/HDDS-16568?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18129680#comment-18129680
]
Siyao Meng commented on HDDS-16568:
-----------------------------------
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, and severity classification.
h3. Run environment
{noformat}
Ozone commit: 20d95ed37fe35013b5320713665db03c06ee36fa
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 28m agent time, 115.1M tokens, about $72 (estimate)
{noformat}
h3. Result
19 candidate findings came out of model checking (7) and code review (12), and
all 19 were investigated individually.
||Disposition||Count||
|Reproduced|13|
|Masked (defect present, harm prevented by another component today)|2|
|False positive|2|
|Dropped as already reported|2|
Most reproduced findings share one pattern: a volume, bucket or key is checked
once before the request is applied, or read from a stale source, and a same
name delete and recreate or an unflushed write changes it in between. Findings
that share one fix are one issue, so the 13 reproduced findings are 10 issues.
Each issue was 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, reproduction and report were
reviewed independently before filing. One of the two masked findings is filed
as well, because the fix is small and the request is otherwise stored on a
bucket it was never validated against. Three further defects were found during
review of the fixes and are filed separately.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17249|Major|Snapshot create does not check the bucket again at apply|
|HDDS-17248|Major|Deleted keys moved out of a deleted snapshot lose their
bucket ID, so their purge reduces the usage of a later bucket of the same name|
|HDDS-17240|Major|Quota repair rolls back unflushed volume changes and writes
converted volumes under the bare volume name|
|HDDS-17250|Major|Key commit does not check that an object store open key
belongs to the current bucket of that name|
|HDDS-17237|Major|Tenant create on a Kerberos cluster overwrites the creating
admin's volume list, so their existing volumes disappear from listVolumes|
|HDDS-17238|Major|Volume create takes refCount and usedNamespace from the
request instead of initializing them to 0|
|HDDS-17239|Major|Bucket create takes usedBytes, usedNamespace and the snapshot
usage counters from the request instead of initializing them to 0|
|HDDS-17247|Major|FSO multipart upload completed under a recreated parent
directory builds a new open key instead of reusing the one created at initiate|
|HDDS-17241|Major|Quota repair can leave bucket snapshotUsedBytes negative when
a snapshot purge commits after the repair's checkpoint and before the snapshot
scan|
|HDDS-17246|Minor|Lifecycle task can create the previous owner's .Trash
directory in a bucket that was deleted and recreated while the task ran|
|HDDS-17245|Minor|SetLifecycleConfiguration validated against one bucket can be
stored on a different bucket created under the same name before it is applied|
Found during review of the fixes above:
||Issue||Priority||Summary||
|HDDS-17243|Major|Quota repair counts pending deletes of a bucket again for
every snapshot of another bucket that holds a copy of them|
|HDDS-17244|Major|Quota repair skips deleted snapshots that are not purged yet,
so the pending deletes they still hold drop out of the bucket's
snapshotUsedBytes|
|HDDS-17251|Minor|ozone admin om list-open-files fails with
NumberFormatException when an open multipart upload is in the listed range|
Priorities follow the manual validation, not the pipeline's severity classes.
Every issue has a proposed fix patch with a regression test. HDDS-17237,
HDDS-17240, HDDS-17241, HDDS-17243, HDDS-17244, HDDS-17246, HDDS-17248 and
HDDS-17251 also have a standalone reproduction test attached; for the others
the regression tests in the patch show the behaviour.
h3. Not filed
* Masked: a deleted bucket's lifecycle scan state row is not removed. The rows
are bounded by the number of distinct deleted bucket names, and the only reader
discards rows whose bucket object ID does not match.
* False positive: a bucket delete that writes cache tombstones before a volume
check. The throw is unreachable under the earlier volume check and the volume
lock.
* False positive: a multipart upload initiate check that runs only before
apply. The check made again when parts are committed prevents any effect.
* Dropped as already reported: tenant delete checking that the tenant is empty
only before apply (HDDS-16856), and a rejected part commit leaving its open key
(HDDS-16785).
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-resource-deletion-gates|apache/ozone|Java|Use the target-specific
guidance"
{code}
h3. Caveats
* HDDS-17240 needs a volume change applied but not yet flushed when a full
quota repair is applied, and a volume still carrying the pre 1.1 quota value.
The tests control when the double buffer flushes. It was not run on a three OM
cluster.
* HDDS-17241 needs a snapshot purge to commit between the repair's checkpoint
and the scan of that snapshot. The reproduction commits the purge at that
point; the fix fails the repair run in that case, and rerunning it is safe.
* HDDS-17246 was reproduced with the lifecycle service's existing pause hook.
The patch reduces it to a single request; closing it fully is described in the
issue as a follow up.
* HDDS-17249 and HDDS-17245 were shown through the request classes against a
real OM metadata store, not on a cluster.
* HDDS-17243 and HDDS-17244 apply on top of the patch of HDDS-17241, and
HDDS-17244 should land with or after HDDS-17243. HDDS-17249 touches the same
lines of OMSnapshotCreateRequest as the open pull request apache/ozone#10965.
* The patches were built and tested on the pinned commit, all 14 apply together
on it, and each applies to master at 64d4a791502 (HDDS-17243 and HDDS-17244
with the patch of HDDS-17241 first).
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-resource-deletion-gates (Apache Ozone master @20d95ed)
> --------------------------------------------------------------------------
>
> Key: HDDS-16568
> URL: https://issues.apache.org/jira/browse/HDDS-16568
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: om-resource-deletion-gates.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-resource-deletion-gates}}. Scope and code entry points are in the
> attached guidance file [^om-resource-deletion-gates.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: 20d95ed37fe35013b5320713665db03c06ee36fa
> 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-resource-deletion-gates|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]
