[
https://issues.apache.org/jira/browse/HDDS-16569?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18129768#comment-18129768
]
Siyao Meng commented on HDDS-16569:
-----------------------------------
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: b10a7d427bdf83807a7e48a1be507d3b02d5a503
Specula: v1.2.0-34-gcdd19e39, with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 40G memory, 20 workers
Total: 5h 47m agent time, 122.1M tokens, about $63 (estimate)
{noformat}
h3. Result
6 candidate findings came out of model checking (4) and code review (2), and
all 6 were investigated individually.
||Disposition||Count||
|Reproduced|2|
|Masked (defect present in code that has no production caller yet)|3|
|Dropped as already reported|1|
Each reproduced finding 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 and report were reviewed
independently before filing.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17259|Major|Compaction DAG is populated without the lock its readers
take, so snapshot diff can miss keys and backup SST pruning can silently stop|
|HDDS-17260|Major|Snapshot diff can omit changed keys whose names differ from a
nearby key by a supplementary character against a character in U+E000 to U+FFFF|
Priorities follow the manual validation, not the pipeline's severity classes.
Both issues have a proposed fix patch with regression tests. HDDS-17259 also
has a standalone reproduction test attached; for HDDS-17260 the regression
tests in the patch show the behaviour.
h3. Not filed
* Masked: three defects in the optimized snapshot diff components (the sequence
gated DAG reader and the merge join report builder), which have no production
caller at this commit. They become reachable with apache/ozone#11651 behind a
default off setting, so they are better handled in that pull request. They were
shown at the component level only.
* Dropped as already reported: one finding duplicates HDDS-16442.
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-snapshot-diff-semantics|apache/ozone|Java|Use the target-specific
guidance"
{code}
h3. Caveats
* HDDS-17259 needs a snapshot diff to walk the compaction DAG while the
compaction listener is adding the edges of one compaction. The reproduction
pauses the listener after its first edge; 300 rounds without the pause did not
hit the window. That a stopped pruning task stays stopped until the OM restarts
or reopens its DB was checked with a unit test, not on a cluster.
* HDDS-17260 was run without the native RocksDB tools library; the native
library path uses the same merge and is argued from code. The effect on
incremental snapshot defragmentation (off by default) is also argued from code.
* The patches were built and tested on the pinned commit and apply to master at
d3b5f518556. HDDS-17260 touches SnapshotDiffManager, which apache/ozone#11651
also changes, in different methods.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-snapshot-diff-semantics (Apache Ozone master @b10a7d4)
> --------------------------------------------------------------------------
>
> Key: HDDS-16569
> URL: https://issues.apache.org/jira/browse/HDDS-16569
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: om-snapshot-diff-semantics.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-diff-semantics}}. Scope and code entry points are in the
> attached guidance file [^om-snapshot-diff-semantics.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: b10a7d427bdf83807a7e48a1be507d3b02d5a503
> 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-diff-semantics|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]
