[
https://issues.apache.org/jira/browse/HDDS-16545?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18127051#comment-18127051
]
Siyao Meng commented on HDDS-16545:
-----------------------------------
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: 1fb64c8e499161d1452ae6948ffd461fc9d2c302
Specula: v1.2.0-27-g0263f82a, with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 1h 47m agent time, 85.5M tokens, about $57 (estimate)
{noformat}
h3. Result
6 candidate findings came out of model checking (4) and code review (2), and
all 6 were investigated individually. No spec repair requests were raised by
confirmation.
||Disposition||Count||
|Reproduced|5|
|False positive|1|
The five reproduced findings need five separate fixes, so they are five 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-14), and the fix patch, reproduction and report were
reviewed independently before filing. One further defect in the same code was
found during that review and is filed as well.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17000|Critical|Sequential read retried after a failed ReadChunk silently
skips the bytes it had already copied from the chunk buffer|
|HDDS-16999|Major|EC reconstruction read returns data of the wrong stripe after
it switches an index to a spare replica|
|HDDS-17002|Major|Streaming block read after unbuffer() requests nothing at the
current position, times out and excludes a healthy datanode|
|HDDS-17004|Major|Streaming block read does not try another replica after a
client side checksum mismatch|
|HDDS-17003|Major|Interrupted EC reconstruction read returns while its cell
reads still write into stripe buffers that close() gives back to the buffer
pool (found during review)|
|HDDS-17001|Minor|EC reconstruction read returns unfilled stripe buffers when
the stream is read again after a failed read or seek|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch attached, and each except HDDS-17003 a
standalone reproduction test; HDDS-17003 is covered by the regression tests in
its patch.
h3. Not filed
* False positive: a positioned read that lands on an empty interior part or
chunk returns an early EOF. No writer in the tree commits an empty interior
block (the write pools drop zero length blocks, multipart parts have a minimum
size, lease recovery only appends at the end), so the state is unreachable.
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 \
"client-read-retry|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17000 was reproduced with a simulated datanode transport on the real
client stack, not on a cluster. HDDS-16999 and HDDS-17001 used the client test
replica streams.
* HDDS-17002 and HDDS-17004 affect only streaming block reads
({{ozone.client.stream.readblock.enable}}, off by default). For HDDS-17004 on
current code the failure shows first as a false EOF from HDDS-16680; streaming
reads of a block with one corrupt replica succeed only with both fixes.
* HDDS-17001 needs an application that catches the exception and reads the same
stream again; no in-tree caller does.
* The patches were built and tested on the pinned commit and apply to master at
fd2f6092c6d. HDDS-17001 and HDDS-17003 touch the same test imports, so the
second one to land needs a trivial rebase.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify client-read-retry (Apache Ozone master @1fb64c8)
> -----------------------------------------------------------------
>
> Key: HDDS-16545
> URL: https://issues.apache.org/jira/browse/HDDS-16545
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: client-read-retry.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
> {{client-read-retry}}. Scope and code entry points are in the attached
> guidance file [^client-read-retry.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: 1fb64c8e499161d1452ae6948ffd461fc9d2c302
> 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 \
> "client-read-retry|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]
