[jira] [Created] (HDDS-16471) [Specula] Verify om-fso-namespace (Apache Ozone @9fbf9ee)

["Siyao Meng (Jira)" <ji...@apache.org>]

Siyao Meng created HDDS-16471:
---------------------------------

             Summary: [Specula] Verify om-fso-namespace (Apache Ozone @9fbf9ee)
                 Key: HDDS-16471
                 URL: https://issues.apache.org/jira/browse/HDDS-16471
             Project: Apache Ozone
          Issue Type: Sub-task
            Reporter: Siyao Meng
         Attachments: om-fso-namespace.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-fso-namespace}}. Scope and code entry points are in the attached guidance file [^om-fso-namespace.guidance.md].

h3. Run environment
{noformat}
Apache Ozone commit: 9fbf9ee0cb1bd2f5f5d437b6719ebbe5309351fb
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-fso-namespace|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
* 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: issues-unsubscribe@ozone.apache.org
For additional commands, e-mail: issues-help@ozone.apache.org