[
https://issues.apache.org/jira/browse/HDDS-16470?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18125918#comment-18125918
]
Siyao Meng commented on HDDS-16470:
-----------------------------------
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, the spec repair loop, and severity
classification.
h3. Run environment
{noformat}
Ozone commit: 20e6a1c0f6039248373efd3eb1d7f2afcf7f1535
Specula: v1.2.0
Agent/model: claude-code, Claude Opus 5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 6h 51m agent time, 265.8M tokens, about $220
{noformat}
h3. Result
15 candidate findings were consolidated from model checking (MC-1 to MC-6) and
code review (CR-1 to CR-9). The spec repair loop ran two rounds, resolved all 8
repair requests, and surfaced 4 more model checking violations (MC-7 to MC-10).
All 19 were investigated individually.
||Disposition||Count||
|Reproduced|3|
|False positive|14|
|Dropped (already tracked upstream)|2|
Severity of the 3 reproduced findings: 2 Critical, 1 High. All three reached
debate consensus. MC-2 and MC-4 were confirmed three times each, once in the
first pass and once in each repair round.
h3. Reproduced findings
* (Critical) The dedup record keyed by {{ClientInvocationId(clientId, callId)}}
lives only in the in-memory Ratis retry cache. Nothing persists or rebuilds it,
while the Raft log and the applied index are durable. After a clean OM restart,
a client retry of a write that already committed and applied misses
{{checkRetryCache}}, runs {{preExecute}} again, and a second log entry with the
same invocation ID is committed and applied. Reproduced with {{renameKey}}: the
rename that succeeded is reported to the caller as {{KEY_ALREADY_EXISTS}}.
[MC-2]
* (High) The retry cache probe, {{preExecute}}, and the Ratis submit are three
separate steps. {{checkRetryCache}} is a read-only {{getIfPresent}}, and the
record it looks for is created only inside the Ratis submit, after
{{OMExecutionFlow}} has already run {{preExecute}}. A duplicate attempt that
arrives while the first is still in {{preExecute}} misses the probe, runs
{{preExecute}} a second time, and is only then absorbed by Ratis. For snapshot
create this increments {{inFlightSnapshotCount}} twice and decrements it once,
so with {{ozone.om.fs.snapshot.max.limit}} set to 8 the eighth
{{createSnapshot}} is refused with 7 snapshots present. The leak persists until
a leadership change resets the counter. [MC-4]
* (Critical) {{RetryInvocationHandler}} pins {{Client.callId}} in a ThreadLocal
before every attempt, with no {{finally}}, and only the {{Client.Call}}
constructor clears it. With follower read enabled, a DNS refresh between two
attempts nulls the cached OM proxy, and the next attempt throws in the follower
loop of {{HadoopRpcOMFollowerReadFailoverProxyProvider}} before any RPC is
issued. The pin is never cleared, so every later request on that thread,
including one from an unrelated client to a healthy OM, fails with
{{IllegalStateException}} at {{Client.setCallIdAndRetryCount}}. [CR-4]
h3. Filed
||Finding||Issue||Attachment||
|MC-2|HDDS-16743|proposed fix patch (persists recent replies in the OM DB) with
a regression test, plus the reproduction test alone|
|MC-4|HDDS-16744|fix patch with a regression test|
|CR-4|HDDS-16745|fix patch with a regression test|
h3. Novelty
* MC-4 and CR-4 were classified as new. HDDS-13357 touches
{{inFlightSnapshotCount}} accounting but not the probe gap.
* MC-2 was classified as known and unfixed, with HDDS-16736 as the nearest
existing issue. HDDS-16736 covers the S3 gRPC trigger for the same dependency
of non idempotent requests on the retry cache. The restart trigger here is a
different path on the default Hadoop RPC transport, so it is filed separately
as HDDS-16743.
h3. Dropped
* CR-6: two configuration keys set the same retry cache expiry. Tracked by
HDDS-16254.
* CR-8: {{getOMResponseFromRaftClientReply}} dereferences the reply message
with no null guard. Tracked by HDDS-11360.
h3. False positives
MC-1, MC-3, MC-5 to MC-10, CR-1 to CR-3, CR-5, CR-7 and CR-9 were investigated
and dismissed. Notable negatives: the retry cache record is rebuilt on every
replica that applies the entry, so a plain failover to a surviving peer is
covered (MC-3); Hadoop RPC pins one {{(clientId, callId)}} per logical
invocation across attempts (CR-1); the client ack follows the Raft log fsync
and commit (CR-3).
h3. Reproduce
{code:none}
specula run --agent=claude-code --effort=medium --model='claude-opus-5[1m]' \
--max-parallel=2 --enable-reviews --confirm-debate \
--tlc-memory-limit=28G --tlc-worker-limit=8 \
"om-retry-cache|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* MC-2 holds for a single OM, a whole cluster restart, or a restarted node that
regains leadership. It needs the entry to have been flushed to the OM DB before
the restart: an OM that stops before the flush replays the entry from the Raft
log and recreates the record. Its reproduction reused the instrumented harness
checkout at the same commit; both agents checked that the trace instrumentation
does not affect dedup.
* MC-4 was reproduced with timing assistance only (two attempts of one
invocation released from a latch, no product code modified). Only the snapshot
counter consequence was demonstrated. The same ordering applies to other
{{preExecute}} side effects such as SCM {{allocateBlock}}, but those were
argued, not exercised.
* CR-4 needs both {{ozone.client.follower.read.enabled}} and
{{ozone.client.failover.resolve-needed}}, which default to false. Its scope was
narrowed during the debate to the follower loop arm; the other exits named in
the original candidate were conceded as unreachable.
* The first confirmation pass rejected the issue records for MC-4 and CR-4 on
format, and the run had to be restarted by hand to record them. Their
investigator and Challenger verdicts did not change.
* Model checking and trace validation ran against 9 collected trace scenarios
covering dedup hit, the probe gap, failover, expiry, restart, invocation
identity, stale reply, NotLeader, and the S3 auth path.
Generated with Specula (Claude Opus 5).
> [Specula] Verify om-retry-cache (Apache Ozone master @20e6a1c)
> --------------------------------------------------------------
>
> Key: HDDS-16470
> URL: https://issues.apache.org/jira/browse/HDDS-16470
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: om-retry-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-retry-cache}}. Scope and code entry points are in the attached guidance
> file [^om-retry-cache.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-retry-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
> * 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]
