[
https://issues.apache.org/jira/browse/HDDS-16472?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18124917#comment-18124917
]
Siyao Meng commented on HDDS-16472:
-----------------------------------
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: d067ba38e7aea917db7efd290b4af53987ec985a
Specula: v1.2.0
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 4h 31m agent time, 68.3M tokens, about $60 (estimate)
{noformat}
h3. Result
9 candidate findings came out of model checking (5) and code review (4), and
all 9 were investigated individually. No spec repair requests were raised by
confirmation.
||Disposition||Count||
|Reproduced|6|
|Masked (defect present, harm prevented by another component today)|2|
|False positive|1|
Four reproduced findings share one root cause and one fix, so they are one
issue. 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-08), and the fix patch, reproduction and report were
reviewed independently before filing. One of the two masked findings turned out
to have a consequence that is not masked and is filed as well.
h3. Filed
||Issue||Priority||Summary||
|HDDS-16787|Critical|Part commit that fails on bucket quota leaves the part in
the OM table cache, so a later part commit, abort or complete acts on it|
|HDDS-16786|Major|MultipartUploadCleanupService can build an abort request
larger than the Ratis log entry limit, which makes the OM leader step down|
|HDDS-16788|Major|CompleteMultipartUpload terminates the OM when the open key
of an OBJECT_STORE or LEGACY upload is missing|
|HDDS-16785|Minor|Part commit rejected with NO_SUCH_MULTIPART_UPLOAD_ERROR
leaves its open key behind, so its blocks are queued for deletion twice|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch and a standalone reproduction test attached.
h3. Not filed
* Masked: a failed expired abort request leaves cache tombstones for the
uploads it already processed. The only cause found is a storage read fault, and
the OM terminates on that error before another transaction applies.
* False positive: the expired scan selection is revalidated by name only at
apply. The upload ID in the key name already identifies the generation and
everything else is recomputed at apply.
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-expired-mpu-cleanup|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-16787 needs a request for the same upload to be applied before the OM
has flushed the failed part commit. The reproductions hold the flush with the
existing {{OzoneManagerDoubleBuffer}} pause hook. Without the hook, concurrent
clients hit the window at low rates (for example 3 of 150 rounds, and 2 of 10
on a three OM cluster).
* HDDS-16786 needs more than 32MB of upload names in one scan: about 31,000
expired uploads without parts with 1024 character key names (run), or about
250,000 with ordinary names (calculated).
* HDDS-16788 needs an upload whose open key is missing. No way to create that
state through the client API or the background services was found at this
commit. It can be carried over from 1.3.x.
* The patches were built and tested on the pinned commit and apply to master at
a6332fb5987. HDDS-16785 and HDDS-16787 touch the same test imports, so the
second one to land needs a trivial rebase.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-expired-mpu-cleanup (Apache Ozone master @d067ba3)
> ----------------------------------------------------------------------
>
> Key: HDDS-16472
> URL: https://issues.apache.org/jira/browse/HDDS-16472
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: om-expired-mpu-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-expired-mpu-cleanup}}. Scope and code entry points are in the attached
> guidance file [^om-expired-mpu-cleanup.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: d067ba38e7aea917db7efd290b4af53987ec985a
> 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-expired-mpu-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 ({{20e6a1c}}); use the
> commit above. Its code entry-point line numbers are unchanged on this head.
> 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]