[
https://issues.apache.org/jira/browse/HDDS-17539?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18133967#comment-18133967
]
Siyao Meng commented on HDDS-17539:
-----------------------------------
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: efe0c7eba1527530d1001f6517b733576fdc6d61
Specula: v1.2.0-35-gf5285a2b, with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 6h 3m agent time, 110.6M tokens, about $66 (estimate)
{noformat}
h3. Result
9 candidate findings came out of model checking (6) and code review (3), and
all 9 were investigated individually. Confirmation raised one spec repair
request, which removed one false positive; the remaining counterexamples were
regenerated and confirmed again.
||Disposition||Count||
|Reproduced|4|
|Masked (defect present, harm prevented by another component today)|1|
|False positive|4|
Two pairs of reproduced findings share a fix, so they are two issues. Each
issue 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-28), and the fix patch and report were reviewed
independently before filing. The masked finding is filed as Minor: the defect
is real, and its cost today is extra failovers, not a wrong result. One more
defect was found while reviewing a fix and is filed as well; it is not counted
above.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17548|Major|OM client turns follower read off for the rest of its life,
or keeps retrying a not ready leader, after an OM rejects a LOCAL_LEASE read|
|HDDS-17550|Major|OM local lease check never detects a missing leader, so a
leaderless OM or a not ready leader can serve LOCAL_LEASE reads from its local
DB|
|HDDS-17547|Minor|GrpcOmTransport can send to a follower while its failover
provider names the leader, so concurrent failovers move the client away from
the leader|
|HDDS-17549|Minor|Without security, an OM follower runs the preExecute of S3
writes before rejecting them, so a lagging follower can return an error, not
NotLeader (found during review)|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch with a regression test attached.
HDDS-17547, HDDS-17548 and HDDS-17549 also have a standalone reproduction test;
HDDS-17550 has none, and the regression test in its patch shows the behaviour.
h3. Not filed
* MC-6 (false positive): the counterexample needed a request input that the S3
gateway rejects before it reaches the OM client. The spec was corrected and the
violation is gone.
* CR-1, CR-2, CR-3 (false positives, code review): investigated and found not
to be defects at this commit.
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-read-consistency-routing|apache/ozone|Java|Use the target-specific
guidance"
{code}
h3. Caveats
* Landing order: HDDS-17550 makes OMs refuse LOCAL_LEASE reads they used to
answer, and a client without HDDS-17548 reacts to such a refusal badly.
HDDS-17548 should land first or together with HDDS-17550.
* HDDS-17548: the not ready leader part was reproduced with the real client
retry code against simulated OMs, not on a real cluster; no existing hook holds
a newly elected OM not ready with a large apply backlog.
* HDDS-17550: the large stale gap needs the elected OM's DB to be behind its
committed log at restart. The regression test holds the not ready window with
an existing Ratis test injection point.
* HDDS-17547 affects only clients that use the gRPC OM transport
({{ozone.om.transport.class}}). The open pull request for HDDS-17462 changes
the same class and conflicts with its test in one import block.
* HDDS-17549 affects only clusters without security. It was reproduced with the
follower's apply held, not end to end through the S3 gateway. HDDS-15617 has
the same root, and the fix condition needs a second look if that issue changes
how S3 credentials are checked.
* The patches were built and tested on the pinned commit, which is also current
master at efe0c7eba15. All four apply together.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify om-read-consistency-routing (Apache Ozone master @efe0c7e)
> ---------------------------------------------------------------------------
>
> Key: HDDS-17539
> URL: https://issues.apache.org/jira/browse/HDDS-17539
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: om-read-consistency-routing.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-read-consistency-routing}}. Scope and code entry points are in the
> attached guidance file [^om-read-consistency-routing.guidance.md]. Added
> after HDDS-15089, HDDS-16497, HDDS-16737 and HDDS-17448 changed how a read's
> consistency is chosen per request, routed by the Hadoop RPC and gRPC clients,
> and carried to Ratis reads. HDDS-16428 covered the OM read consistency policy
> before these changes.
> h3. Run environment
> {noformat}
> Apache Ozone commit: efe0c7eba1527530d1001f6517b733576fdc6d61
> 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-read-consistency-routing|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
(v10.3.26#10030026)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
