[
https://issues.apache.org/jira/browse/HDDS-16567?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18129473#comment-18129473
]
Siyao Meng commented on HDDS-16567:
-----------------------------------
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: df04bc0e309f625a7dcdcd60790a42f34e2743d9
Specula: v1.2.0-34-gcdd19e39 (with local changes)
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 2h 12m agent time, 61.4M tokens, about $45 (estimate)
{noformat}
h3. Result
10 candidate findings came out of model checking (7) and code review (3), and
all 10 were investigated individually. No spec repair requests were raised by
confirmation.
||Disposition||Count||
|Reproduced|7|
|False positive|3|
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, and the fix patch, reproduction and report were reviewed
independently before filing. Three findings share one fix and are one issue,
two more share another, one of the remaining two is a design issue without a
patch, and one is the defect already reported in HDDS-17200. One finding has
two halves that went to different issues.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17216|Major|S3 secret cache cleanup can remove the entry of an unflushed
transaction, so OMs can commit different S3SecretTable contents|
|HDDS-17214|Major|With an S3 secret store without batch support, a revoke can
delete a newer secret and a store failure at flush time terminates the OM|
|HDDS-17215|Major|OMs call a shared external S3 secret store while applying, so
a late OM can diverge from the leader and a store failure terminates the OM|
Priorities follow the manual validation, not the pipeline's severity classes.
HDDS-17216 and HDDS-17214 have a proposed fix patch attached; HDDS-17214 and
HDDS-17215 have a standalone reproduction test attached. HDDS-17215 needs a
design decision, so it has no patch.
h3. Not filed
* Reproduced, already reported: {{S3SecretManagerImpl.getSecretString}} not
treating a deleted cache entry as absent is HDDS-17200. HDDS-17216 includes the
same change so that it is complete on its own.
* False positive: a lost reply to a secret creation cannot be fetched again
after the retry cache expires. A secret is shown only once by design.
* False positive: flush time store calls of S3 set and revoke do not take
{{S3_SECRET_LOCK}} while the tenant ones do. The asymmetry causes no wrong
result of its own; the lost secret comes from the ordering defect in HDDS-17214.
* False positive: {{clearS3Cache}} uses the lock key "cache", which an access
ID can also have. That only causes brief contention on one lock stripe.
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-s3-secret-cache|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17216 depends on when each OM's double buffer flush runs relative to its
apply thread. Its regression tests turn the interleavings into a plain sequence
of calls, and the two OM case was also run with the real flush method on two OM
stacks in one JVM. How often the interleavings occur in production was not
measured.
* HDDS-17214 and HDDS-17215 were run against an in memory store with the
contract of {{VaultS3SecretStore}}; no Vault server was used, and the multi OM
cases ran as OM stacks in one JVM without Ratis. The termination loop after a
restart in HDDS-17215 and its symptom 2 are argued from the code.
* HDDS-17216 and HDDS-17214 edit the same lines in {{S3RevokeSecretRequest}},
{{OMTenantRevokeUserAccessIdRequest}} and {{TestS3GetSecretRequest}}, so the
second one to land needs a rebase. HDDS-17216's {{getSecretString}} hunk is
dropped if HDDS-17200 is committed first.
* The patches were built and tested on the pinned commit and apply to master at
2cb1b6dd4e9.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-s3-secret-cache (Apache Ozone master @df04bc0)
> ------------------------------------------------------------------
>
> Key: HDDS-16567
> URL: https://issues.apache.org/jira/browse/HDDS-16567
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: om-s3-secret-cache.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-s3-secret-cache}}. Scope and code entry points are in the attached
> guidance file [^om-s3-secret-cache.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: df04bc0e309f625a7dcdcd60790a42f34e2743d9
> 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-s3-secret-cache|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]
