[jira] [Commented] (HDDS-16471) [Specula] Verify om-fso-namespace (Apache Ozone master @20e6a1c)

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

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

Siyao Meng commented on HDDS-16471:
-----------------------------------

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.

h3. Run environment
{noformat}
Ozone commit: 20e6a1c0f6039248373efd3eb1d7f2afcf7f1535
Specula:      v1.2.0
Agent/model:  claude-code, Claude Opus 5.5 (1M context)
Effort:       medium
TLC limits:   28G memory, 8 workers
Total:        5h 43m agent time, 126.6M tokens, about $104 (estimate)
{noformat}

h3. Result
21 candidate findings were consolidated from model checking and code review, and all 21 were investigated individually. The spec converged in one validation round with no spec repair requests.

||Disposition||Count||
|Reproduced|16|
|False positive|2|
|Dropped (already tracked upstream)|3|

Two reproduced findings share one root cause, so 15 issues result. Each one was then validated a second time by hand against the pinned commit: a regression test was added to an existing suite, shown to fail without the fix and pass with it, and the bug was confirmed still present on apache master (checked on 2026-10-07). All 15 held up. 14 are filed below with a proposed fix patch attached. One is reported separately and is not listed here.

h3. Filed
||Issue||Priority||Summary||
|HDDS-16762|Critical|FSO rename to the bucket root silently replaces or shadows an existing root entry and orphans its subtree|
|HDDS-16763|Critical|A failed FSO CompleteMultipartUpload leaves missing parent directories in the cache, so later acknowledged creates become orphans|
|HDDS-16764|Critical|DeleteOpenKeys removes a key hsync'ed after the cleanup scan and queues its blocks for deletion, and the next overwrite commit terminates the OM|
|HDDS-16766|Critical|FSO directory delete emptiness check races with flush and cache eviction, so OMs apply the same delete differently|
|HDDS-16768|Critical|Single key delete of an hsync'ed FSO file persists DELETED_HSYNC_KEY under the wrong open table key|
|HDDS-16765|Major|A rejected overwrite commit leaves OVERWRITTEN_HSYNC_KEY on another writer's cached open entry|
|HDDS-16767|Major|RecoverLease soft limit check uses the local wall clock at apply, so OMs diverge on the same log entry|
|HDDS-16769|Major|OMKeyRenameResponseWithFSO reads the bucket ID at flush time and terminates the OM if the bucket was deleted|
|HDDS-16770|Major|FSO rename response serializes the live cached OmBucketInfo, corrupting bucket usage after crash and replay|
|HDDS-16771|Major|CompleteMultipartUpload over an hsync'ed key does not flag the hsync writer's open entry|
|HDDS-16772|Major|Default ACLs of new keys and directories come from the applying OM's local group mapping, so OMs can store different ACLs|
|HDDS-16773|Major|DeleteKeys with a key listed twice releases bucket quota twice|
|HDDS-16774|Major|CreateDirectory and CreateFile accept '.' and '..' path components on FSO buckets|
|HDDS-16775|Major|Renaming an ancestor of an hsync'ed file breaks its lease expiry auto commit|

Priorities follow the manual validation, not the pipeline's severity classes. HDDS-16764, HDDS-16771 and HDDS-16772 turned out not to be limited to FSO buckets.

h3. Novelty
All were classified as new after searching HDDS issues and apache/ozone pull requests. Nearest existing issues, each a different site or mechanism: HDDS-16117 (HDDS-16763), HDDS-14600 (HDDS-16766), HDDS-6934 (HDDS-16769), HDDS-10650 (HDDS-16768), HDDS-16125 (HDDS-16770), HDDS-16732 (HDDS-16764). HDDS-16772 is scoped to stored default ACLs. ACL checks and bucket link resolution in apply are already tracked by HDDS-13634 and HDDS-15460.

h3. Dropped
* Single FSO key delete decrements the cached bucket before a fallible read. Fixed by HDDS-16161.
* Namespace accounting of overwrite commits on versioned buckets. Matched to HDDS-16175, reproduction not attempted.
* A checkpoint install that does not proceed resumes with the old table caches. Tracked by HDDS-16275, reproduction not attempted.

h3. False positives
* A recovery commit does not require the {{LEASE_RECOVERY}} flag. The missing check grants nothing new.
* Bucket delete checks only root level children. Designed behaviour, no consequence observed.

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

h3. Caveats
* HDDS-16765, HDDS-16766, HDDS-16769 and HDDS-16770 need flush timing that the tests control through the existing {{OzoneManagerDoubleBuffer}} pause hook. The natural windows are narrow.
* Cross OM divergence is argued from single OM and unit level reproductions, not observed on a multi OM cluster.
* HDDS-16764 needs an hsync to land between the cleanup scan and its {{DeleteOpenKeys}} request, a window of milliseconds per service run with default settings.
* HDDS-16771 needs hsync to be enabled, which is off by default.
* HDDS-16773: only the namespace path for zero byte keys exceeds quota. The bytes quota bypass did not reproduce.
* HDDS-16774 needs a raw OM client. The Hadoop filesystem clients normalize paths first.
* HDDS-16767 and HDDS-16772 add an optional proto field. Wire compatibility was reviewed by reading, the compatibility check was not run.
* The patches were built and tested on the pinned commit. All apply to master except one test hunk of HDDS-16773, which needs a mechanical rebase after HDDS-16161. Some patches touch the same lines and need rebasing on each other: HDDS-16769 with HDDS-16770, HDDS-16764 with HDDS-16765.
* The patches are proposals for review.

Generated with Specula (Claude Opus 5.5).


> [Specula] Verify om-fso-namespace (Apache Ozone master @20e6a1c)
> ----------------------------------------------------------------
>
>                 Key: HDDS-16471
>                 URL: https://issues.apache.org/jira/browse/HDDS-16471
>             Project: Apache Ozone
>          Issue Type: Sub-task
>            Reporter: Siyao Meng
>            Assignee: Siyao Meng
>            Priority: Minor
>              Labels: help-wanted, specula
>         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: 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 \
>   "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
> * 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: issues-unsubscribe@ozone.apache.org
For additional commands, e-mail: issues-help@ozone.apache.org