[
https://issues.apache.org/jira/browse/HDDS-16478?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18125906#comment-18125906
]
Siyao Meng commented on HDDS-16478:
-----------------------------------
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: a6b7bdb937109ba2893688b41a89470bc95c88cf
Specula: v1.0.0-56-g62f63a1e (with local changes)
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 40G memory, 20 workers
Total: 5h 54m agent time, 85.4M tokens, about $47 (estimate)
{noformat}
h3. Result
7 candidate findings came out of model checking (5) and code review (2), and
all 7 were investigated individually.
||Disposition||Count||
|Reproduced|7|
Two reproduced findings share one fix and are one issue, and one is a duplicate
of another reproduced finding and is part of its 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-10), and the fix patch, reproduction and report were reviewed
independently before filing. One further issue was found during that review.
h3. Filed
||Issue||Priority||Summary||
|HDDS-16850|Critical|After an OBS or LEGACY rename and recreate of an hsync'ed
key, the hard lease auto commit empties the new key and deletes blocks still in
use|
|HDDS-16851|Critical|Open key cleanup deletes an overwrite in progress when the
overwritten key is older than the expire threshold, so its commit fails|
|HDDS-16848|Major|Hard lease auto commit built before a later hsync shrinks the
key below the length OM acknowledged and deletes the acknowledged block|
|HDDS-16849|Major|OBS/LEGACY key rename does not reject an hsync'ed key as FSO
does|
|HDDS-16847|Major|Hsync key committed by OpenKeyCleanupService after the lease
hard limit is stored with modification time 0|
|HDDS-16852|Major|Reserve the OM owned hsync key metadata names at the request
boundary and tolerate an invalid stored hsync client id in its readers (found
during review)|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch attached, and all but HDDS-16849 and
HDDS-16852 also have a standalone reproduction test; those two are covered by
the regression tests in their patches.
h3. Not filed
* Nothing. The duplicate finding (the auto commit skipping the request's
{{preExecute}}) is covered by HDDS-16847, where only its modification time part
holds.
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=40G --tlc-worker-limit=20 \
"om-open-key-cleanup|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-16847, HDDS-16848, HDDS-16849 and HDDS-16850 need hsync enabled
({{ozone.hbase.enhancements.allowed}} and {{ozone.fs.hsync.enabled}}, both off
by default). HDDS-16851 happens with the default configuration, at the next
open key cleanup run.
* HDDS-16848 needs a block allocation and hsync inside a window of one to a few
Ratis round trips after the cleanup scan. The reproduction holds that window
with a pause after the real scan; only the DEFAULT layout was run, the FSO path
is argued from code.
* HDDS-16848, HDDS-16849 and HDDS-16850 add an OM version through
{{OMVersionManager}} (HDDS-16848 and HDDS-16850 the same
{{HSYNC_COMMIT_VALIDATION}} constant). The number 101 is a placeholder to be
agreed at merge. HDDS-16851 changes a stored timestamp without a version gate,
as its description explains.
* HDDS-16848, HDDS-16850 and HDDS-16852 change the same commit request classes,
so whichever lands later needs a rebase. HDDS-16850 also explains why the scan
change in the patch attached to HDDS-16768 needs to be limited to FSO buckets.
* The patches were built and tested on the pinned commit and apply to master at
b0aa6475b78.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-open-key-cleanup (Apache Ozone master @a6b7bdb)
> -------------------------------------------------------------------
>
> Key: HDDS-16478
> URL: https://issues.apache.org/jira/browse/HDDS-16478
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: om-open-key-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-open-key-cleanup}}. Scope and code entry points are in the attached
> guidance file [^om-open-key-cleanup.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: a6b7bdb937109ba2893688b41a89470bc95c88cf
> 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-open-key-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. 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]
