[
https://issues.apache.org/jira/browse/HDDS-17628?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Siyao Meng updated HDDS-17628:
------------------------------
Description:
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.
was:
Placeholder for a future Specula target. Do not run it yet.
This target will verify the optimized snapshot diff path from HDDS-9154: the
key ordered merge of the two snapshots with a dependency ordered report
(HDDS-15390, HDDS-15391, HDDS-15393, HDDS-15394), which HDDS-15397 put behind
{{ozone.om.snapshot.diff.optimized.enabled}} (default false). Work under
HDDS-9154 is still open: HDDS-15400 (enable it by default and deprecate the old
path), HDDS-15401 (remove the flag), HDDS-15402 (remove the old code),
HDDS-15399 and HDDS-16058. HDDS-16569 ({{om-snapshot-diff-semantics}}) ran
before the optimized path was reachable and did not include it.
h3. When to revisit
Once the remaining HDDS-9154 work is resolved (at least HDDS-15400 and
HDDS-15402): write the guidance at the master commit of that time, attach it,
retitle this issue to the usual "[Specula] Verify om-snapshot-diff-optimized
(Apache Ozone master @<sha>)" form, and add the help-wanted label. Until then
the title does not follow that form on purpose, so tooling that picks the next
open target skips it.
h3. Scope sketch
* Whether the report matches the legacy path for the same pair of snapshots,
including renames, deletes of parents and children, and pagination.
* Whether applying the dependency ordered report in order to the older snapshot
yields the newer one.
* Job submission, resubmission, cancellation, OM restart and leader change
while a job runs.
Report equivalence alone may be better served by a differential property test
against the legacy path; a model should focus on ordering and the job lifecycle.
Summary: [Specula] Verify om-snapshot-diff-optimized (Apache Ozone
master @d3b75c7) (was: [Specula] Verify om-snapshot-diff-optimized
(placeholder until HDDS-9154 is complete))
> [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]
