[
https://issues.apache.org/jira/browse/HDDS-16481?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18129394#comment-18129394
]
Siyao Meng commented on HDDS-16481:
-----------------------------------
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: a6b7bdb937109ba2893688b41a89470bc95c88cf
Specula: v1.2.0-25-g62f63a1e (with local changes)
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 40G memory, 20 workers
Total: 11h 24m agent time, 129.5M tokens, about $86 (estimate)
{noformat}
h3. Result
15 candidate findings came out of model checking (6) and code review (9), and
all 15 were investigated individually.
||Disposition||Count||
|Reproduced|8|
|Masked (defect present, harm prevented by another component today)|3|
|False positive|4|
Each reproduced finding 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-10-20), and the fix patch and report were
reviewed independently before filing. One further defect was found during that
review and is filed as well (HDDS-17200).
h3. Filed
||Issue||Priority||Summary||
|HDDS-17198|Critical|Force creating a tenant on a volume already used by
another tenant terminates every OM, also on restart|
|HDDS-16856|Major|Tenant delete racing a user assign succeeds on a non-empty
tenant and leaves an orphan accessId that stops OM restart|
|HDDS-16858|Major|Tenant requests release the authorizer write lock only in
their apply, so a request that is not applied on this OM leaves the lock held
and later tenant operations time out|
|HDDS-16855|Major|Tenant create that fails in Ranger after creating the admin
role leaves the role behind, so the tenant can never be created again|
|HDDS-17199|Major|OMTenantCreateRequest does not pass the requested volume to
TenantOp.createTenant, so the default tenant policies do not cover the tenant
volume|
|HDDS-17197|Major|Tenant assign and create add table cache entries before a
check that can fail, so a rejected assign can leave a dangling accessId|
|HDDS-16859|Major|Ranger background sync pushes the role members loaded at the
start of the attempt instead of the current ones|
|HDDS-17200|Major|S3SecretManagerImpl.getSecretString ignores the deleted
marker of an S3 secret cache entry and returns its secret|
|HDDS-16854|Minor|Ranger background sync never retries a failed role delete of
a removed tenant, so the tenant can never be created again|
|HDDS-16857|Minor|Ranger background sync deletes the default policies of a
tenant whose create is applied but not yet flushed to RocksDB|
|HDDS-16853|Minor|OM snapshot install leaves the previous multi-tenant manager
and its Ranger background sync running|
|HDDS-17196|Minor|Tenant admin request is rejected with PERMISSION_DENIED while
an admin revokes another accessId of the same user|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch with a regression test attached.
HDDS-16853, HDDS-16854, HDDS-16855, HDDS-16856 and HDDS-16857 also have a
standalone reproduction test; the others have none. The three masked findings
(HDDS-16853, HDDS-16857, HDDS-16859) are filed because the manual validation
found each defect worth fixing on its own. HDDS-16855 is narrower than the open
HDDS-16188, which covers recovery of tenant creation in general.
h3. Not filed
* The four false positives were judged not to hold on a running OM: a case that
occurs only under a Ranger misconfiguration that is already warned about and
recovers once fixed, a state that no shipped caller produces, fields that are
safely published through the Ratis ordering, and a documentation mismatch whose
consequences are covered by other entries.
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=40G --tlc-worker-limit=20 \
"om-ranger-tenancy|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17198 requires cluster admin rights. HDDS-17198 and HDDS-17199 change
the same create request; their patches apply together.
* The Ranger client implementation was not exercised; the tenant tests use the
in memory access controller in place of Ranger.
* The patches were built and tested on the pinned commit and apply to master at
1753288f333.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-ranger-tenancy (Apache Ozone master @a6b7bdb)
> -----------------------------------------------------------------
>
> Key: HDDS-16481
> URL: https://issues.apache.org/jira/browse/HDDS-16481
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: om-ranger-tenancy.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-ranger-tenancy}}. Scope and code entry points are in the attached
> guidance file [^om-ranger-tenancy.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: a6b7bdb937109ba2893688b41a89470bc95c88cf
> 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-ranger-tenancy|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
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
