You are viewing a plain text version of this content. The canonical link for it is here.
Posted to issues@ozone.apache.org by "Siyao Meng (Jira)" <ji...@apache.org> on 2026/10/22 18:58:00 UTC
[jira] [Updated] (HDDS-16576) [Specula] Verify rocksdb-handle-lifecycle (Apache Ozone master @bf3829e)
[ https://issues.apache.org/jira/browse/HDDS-16576?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel ]
Siyao Meng updated HDDS-16576:
------------------------------
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
{{rocksdb-handle-lifecycle}}. Scope and code entry points are in the attached guidance file [^rocksdb-handle-lifecycle.guidance.md].
h3. Run environment
{noformat}
Apache Ozone commit: bf3829e6c8ac69ae17585585703f91426dcdf6b3
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 \
"rocksdb-handle-lifecycle|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.
was:
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
{{rocksdb-handle-lifecycle}}. Scope and code entry points are in the attached guidance file [^rocksdb-handle-lifecycle.guidance.md].
h3. Run environment
{noformat}
Apache Ozone commit: 20e6a1c0f6039248373efd3eb1d7f2afcf7f1535
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 \
"rocksdb-handle-lifecycle|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.
Summary: [Specula] Verify rocksdb-handle-lifecycle (Apache Ozone master @bf3829e) (was: [Specula] Verify rocksdb-handle-lifecycle (Apache Ozone master @20e6a1c))
> [Specula] Verify rocksdb-handle-lifecycle (Apache Ozone master @bf3829e)
> ------------------------------------------------------------------------
>
> Key: HDDS-16576
> URL: https://issues.apache.org/jira/browse/HDDS-16576
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: rocksdb-handle-lifecycle.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
> {{rocksdb-handle-lifecycle}}. Scope and code entry points are in the attached guidance file [^rocksdb-handle-lifecycle.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: bf3829e6c8ac69ae17585585703f91426dcdf6b3
> 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 \
> "rocksdb-handle-lifecycle|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
(v10.3.26#10030026)
---------------------------------------------------------------------
To unsubscribe, e-mail: issues-unsubscribe@ozone.apache.org
For additional commands, e-mail: issues-help@ozone.apache.org