[ 
https://issues.apache.org/jira/browse/HDDS-17628?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18140050#comment-18140050
 ] 

Siyao Meng commented on HDDS-17628:
-----------------------------------

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. The optimized path 
was exercised with {{ozone.om.snapshot.diff.optimized.enabled}} set to true.

h3. Run environment
{noformat}
Ozone commit: d3b75c75bf9ad475551202477c3a21a3f4b968b7
Specula:      v1.0.0-66-gf5285a2b, with local changes
Agent/model:  claude-code, Claude Opus 5.5 (1M context)
Effort:       medium
TLC limits:   28G memory, 8 workers
Total:        4h 49m agent time, 155.5M tokens, about $94 (estimate)
{noformat}

h3. Result
24 candidate findings came out of model checking (11) and code review (13), and 
all 24 were investigated individually.

||Disposition||Count||
|Reproduced|17|
|Masked (defect present, harm prevented by another component today)|2|
|False positive|3|
|Dropped as already reported|2|

Two reproduced findings share one root cause and one fix, so they are one 
issue; the other 15 are one issue each. 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-11-06), and the fix 
patch, reproduction and report were reviewed independently before filing. One 
of the two masked findings is covered by the fix of an issue filed here.

h3. Filed
||Issue||Priority||Summary||
|HDDS-17739|Major|Ordered snapshot diff: path reuse skip in the dependency 
graph returns a non replayable order or a false cycle|
|HDDS-17742|Major|Optimized full snapshot diff omits changes once deep cleaning 
or a snapshot purge advances the from snapshot's lastTransactionInfo|
|HDDS-17743|Major|DAG snapshot diff reads value pruned compaction backup SST 
files and drops every change in them|
|HDDS-17744|Major|Optimized snapshot diff omits a file or directory moved into 
a directory that is deleted before its children are purged|
|HDDS-17745|Major|Optimized FSO snapshot diff drops every file change below the 
bucket root when no directory row changed|
|HDDS-17747|Major|DAG snapshot diff misses the DELETE of a directory that is 
deleted and replaced at the same path within one flush|
|HDDS-17735|Minor|Snapshot diff cleanup can delete a job resubmitted during its 
scan, failing the submit or losing the new job|
|HDDS-17736|Minor|Report rows written by a cancelled snapshot diff task after a 
resubmit are never deleted|
|HDDS-17732|Minor|SnapDiffJobStore.close stops at the first RocksDB error and 
leaves the job's temporary column families in the snapshot diff DB until OM 
restart|
|HDDS-17733|Minor|Snapshot diff page token is not checked against the current 
report|
|HDDS-17734|Minor|Optimized snapshot diff of an OBS bucket is labelled 
"dependency ordered" although its entries are not|
|HDDS-17737|Minor|Ordered snapshot diff served by the legacy diff is stored as 
ordered, so a later ordered request never replaces it|
|HDDS-17738|Minor|Ordered snapshot diff fails on every request when the changes 
contain a rename cycle, instead of returning an unordered report|
|HDDS-17740|Minor|Ordered snapshot diff resubmit skips the cleanup grace 
period, so a concurrent read of the DONE report fails|
|HDDS-17741|Minor|OM crash during an ordered snapshot diff resubmit can leave a 
DONE job whose report the cleanup then deletes|
|HDDS-17746|Minor|Optimized snapshot diff merge join compares objectIds as 
signed longs while the lists are in unsigned byte order|

Priorities follow the manual validation, not the pipeline's severity classes. 
Each issue has a proposed fix patch attached, and each except HDDS-17733 also 
has a standalone reproduction test; for HDDS-17733 the regression test in the 
patch is the reproduction.

h3. Not filed
* Masked: a cancelled diff task that keeps running writes its stage and 
progress into the resubmitted job until that job's next update. Display only, 
and the same mechanism as the open HDDS-17401.
* False positive: a cancel racing a resubmit. Every outcome matches some serial 
order of the two requests.
* False positive: the optimized report differs from the legacy report for 
directory MODIFY entries and renames of unchanged keys. This is the designed 
behaviour.
* False positive: an ordering failure is classified by its message text. No 
caller depends on the exception type, and the other throws are not reachable in 
practice.
* Already reported: two findings duplicate open HDDS issues and were not 
refiled.

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-snapshot-diff-optimized|apache/ozone|Java|Use the target-specific 
guidance"
{code}

h3. Caveats
* The optimized snapshot diff is off by default at this commit 
({{ozone.om.snapshot.diff.optimized.enabled}}) and is in no release. All issues 
except HDDS-17735 and HDDS-17736 need it switched on. Those two also affect the 
default path and releases 2.2.0 to 2.2.2. The Major issues should be fixed 
before the optimized diff is enabled by default (HDDS-15400).
* HDDS-17739 should land together with or after HDDS-17738. With HDDS-17739 
alone, some rename shapes go from a wrong ordered report to an ordered request 
that produces no report.
* The reproductions of the DAG path (HDDS-17743, HDDS-17745, HDDS-17747) need 
the native rocks tools library ({{-Drocks_tools_native}}).
* HDDS-17741 needs a crash between two local writes. Its tests simulate it by 
failing the second write. HDDS-17746 needs a bucket holding objectIds from 
Ozone 1.0.0 or earlier, or from a non Ratis OM on 1.1.0 to 1.4.1. Its 
reproduction writes such ids directly, and no real upgrade was run.
* The patches were built and tested on the pinned commit and each applies alone 
to master at bbc8505e00d. Applied together in key order, HDDS-17740 and 
HDDS-17741 conflict with HDDS-17735 and HDDS-17736 in 
{{SnapshotDiffCleanupService}} and {{SnapshotDiffManager}}. HDDS-17738 and 
HDDS-17743 conflict only in test imports or adjacent test additions. HDDS-17735 
and an open pull request change the same lines of 
{{SnapshotDiffCleanupService.run}}.
* The patches are proposals for review.

Generated with Specula (Claude Opus 5.5).

> [Specula] Verify om-snapshot-diff-optimized (Apache Ozone master @d3b75c7)
> --------------------------------------------------------------------------
>
>                 Key: HDDS-17628
>                 URL: https://issues.apache.org/jira/browse/HDDS-17628
>             Project: Apache Ozone
>          Issue Type: Sub-task
>            Reporter: Siyao Meng
>            Assignee: Siyao Meng
>            Priority: Minor
>              Labels: specula
>         Attachments: om-snapshot-diff-optimized.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-optimized}}. Scope and code entry points are in the 
> attached guidance file [^om-snapshot-diff-optimized.guidance.md]. Added as a 
> placeholder while the optimized path from HDDS-9154 was being merged; 
> HDDS-16569 ran before that path was reachable and did not include it.
> h3. Run environment
> {noformat}
> Apache Ozone commit: d3b75c75bf9ad475551202477c3a21a3f4b968b7
> 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-optimized|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
> * 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]

Reply via email to