[
https://issues.apache.org/jira/browse/HDDS-17641?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18136444#comment-18136444
]
Siyao Meng commented on HDDS-17641:
-----------------------------------
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: ec5ed5f7ea0e4b406aee53aae4906616819cba2b
Specula: v1.0.0-66-gf5285a2b (with local changes)
Agent/model: claude-code, Claude Opus 5.5 (1M context), on a Linux lab host
Effort: medium
TLC limits: 40G memory, 20 workers
Total: 4h 24m agent time, 116.0M tokens, about $73 (estimate)
{noformat}
h3. Result
13 candidate findings came out of model checking (3) and code review (10), and
all 13 were investigated individually. One scoped spec repair round was run,
and the two model checking findings it covered were confirmed again after it.
||Disposition||Count||
|Reproduced|3|
|Masked (defect present, harm prevented by another component today)|1|
|False positive|9|
Two reproduced findings share one root cause and one fix, so they are one
issue. 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-11-02), and the fix patch, reproduction and report were
reviewed independently before filing. The masked finding is filed as a Minor
hardening issue, since no supported path reaches it.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17668|Critical|PutBlock reply handlers of a Ratis BlockOutputStream can
run out of order, so close() can commit wrong data and OM can get an older
bcsId|
|HDDS-17669|Major|Interrupting a Ratis key write, hsync or close that waits for
a watch for commit loses the interrupt, and the data is retried on a new block|
|HDDS-17667|Minor|Hardening: AbstractCommitWatcher keeps the cached future of a
failed watch for commit uncompleted, so a repeated watch of that index would
hang|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch and a standalone reproduction test attached.
h3. Not filed (false positives)
* A failed ALL_COMMITTED watch falls back to MAJORITY_COMMITTED for the
pipeline client. This is deliberate, and the data is still majority committed.
* The WriteChunk reply handler calls {{completeExceptionally}} on an already
completed future. The stored stream exception still surfaces the error.
* The {{checkState}} on the removed reply future after cleanup. No caller ever
observes its failure.
* {{close()}} does not take the key write semaphore and can overlap
{{hsync()}}. Only the late hsync fails, and OM never records a wrong key.
* {{BlockOutputStreamEntry.cleanup}} creating a stream to release it. That code
does not run at this commit and is needed for the retry.
* The ExcludeList container and pipeline sets are not concurrent and never
expire. They are only touched under the write lock, and SCM falls back when the
exclusions cover everything.
* The {{committedBlockLength}} in the PutBlock reply is ignored. It only echoes
the client's own chunk list.
* The EOF only PutBlock at close does not update the bcsId. The lower bcsId
always passes the datanode checks and changes no data.
* A follower reported in {{NotReplicatedException}} commit infos is marked
failed. That only happens after the full watch timeout, which is intended.
h3. Reproduce
{code:none}
specula run --agent=claude-code --effort=medium --model='claude-opus-5-5[1m]' \
--max-parallel=4 --enable-reviews --confirm-debate \
--tlc-memory-limit=40G --tlc-worker-limit=20 \
"client-ratis-write-failure|apache/ozone|Java|Use the target-specific
guidance"
{code}
h3. Caveats
* HDDS-17668: the older bcsId needs only reply timing and an unlucky thread
schedule. The wrong committed data also needs a block error in a narrow window,
and was only reproduced with the handler order controlled (the reproductions
replace the client's response executor by reflection). The read failure after a
datanode stop was run with a test only hook that delays follower apply and is
not attached. The hsync variant is from code reading. No benchmark was run for
the patch.
* HDDS-17669 changes behaviour on purpose: with the patch an interrupted
{{write()}}, {{hsync()}} or {{close()}} fails and keeps the interrupt flag,
where today it succeeds silently.
* HDDS-17667 has no user visible effect today.
* The patches were built and tested on the pinned commit and each applies alone
to master at b683fd3f294. Their production changes combine cleanly, but all
three add tests to {{TestBlockOutputStreamCorrectness}} (imports and a test
helper overload), so the second and third to land need a rebase of that test
file.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify client-ratis-write-failure (Apache Ozone master @ec5ed5f)
> --------------------------------------------------------------------------
>
> Key: HDDS-17641
> URL: https://issues.apache.org/jira/browse/HDDS-17641
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: client-ratis-write-failure.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-ratis-write-failure}}. Scope and code entry points are in the
> attached guidance file [^client-ratis-write-failure.guidance.md]. Added as a
> narrower rerun of client-ratis-write (HDDS-16427), which modeled buffer
> release, retry handoff and the hsync barrier at 9fbf9ee and found nothing;
> this one adds failure classification, block length and commit sequence id at
> OM, and pipeline clients shared across streams.
> h3. Run environment
> {noformat}
> Apache Ozone commit: ec5ed5f7ea0e4b406aee53aae4906616819cba2b
> 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-ratis-write-failure|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 ({{ef63bac}}); 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
(v10.3.26#10030026)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
