[
https://issues.apache.org/jira/browse/HDDS-17233?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18131578#comment-18131578
]
Siyao Meng commented on HDDS-17233:
-----------------------------------
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: 7212465c0bb19615708c144238317db51c2a696d
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: 4h 14m agent time, 115.6M tokens, about $68 (estimate)
{noformat}
h3. Result
11 candidate findings came out of model checking (2) and code review (9), and
all 11 were investigated individually.
||Disposition||Count||
|Reproduced|5|
|Masked (defect present, harm prevented by another component today)|1|
|False positive|2|
|Dropped as already reported upstream|3|
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-24), and the fix patch, reproduction and report were
reviewed independently before filing. Two reproduced findings share one fix and
are one issue. One reproduced finding is covered by the fix of an issue found
during validation and is not filed separately. The masked finding has a
consequence that is not masked and is filed as well. Validation and review
found three further defects in the same code, filed below.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17438|Critical|Verify the block token of a stream init like WriteChunk,
and set up a data stream only after its init succeeded|
|HDDS-17439|Critical|Datanode does not check that a PutBlock committed through
a data stream is for the stream's block and carries a valid block token|
|HDDS-17430|Major|After a datanode crash, every PutBlock to a container created
by a Ratis data stream fails updateBCSID, closing the pipeline on log replay|
|HDDS-17431|Major|With PutBlock without Raft, a failed data stream close is
reported as success, so OM commits a block that no replica or only one replica
has|
|HDDS-17435|Major|Replaying a stream init log entry after a datanode restart
recreates a deleted container replica empty, which SCM can count as healthy|
|HDDS-17440|Major|Block token verification should check that the request's
container ID is the container of the token's block|
|HDDS-17432|Minor|Stream PutBlock that passed the open check can commit into a
container after it is closed and its checksum and close report were taken|
HDDS-17435, HDDS-17438 and HDDS-17440 were found during validation and review.
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch attached; HDDS-17438, HDDS-17439 and
HDDS-17440 have no standalone reproduction attached, the others have one.
h3. Not filed
* Covered by HDDS-17435: a stream init with PutBlock replayed for a missing
container fails a precondition. Its fix is part of the HDDS-17435 patch.
* False positive: the client does not wait for the Raft reply of the data
stream link. That reply has no durability, BCSID or replay effect.
* False positive: an end of block PutBlock with bcsId 0 regressing the
container BCSID. It needs injected datanode state that no real write path
produces.
* Already reported upstream: three code review candidates match open issues,
among them HDDS-16824, HDDS-17093 and HDDS-16828.
* HDDS-7552 was re-confirmed on this commit, for Ratis and EC containers;
details are in a comment there.
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 \
"dn-putblock-no-raft|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* PutBlock without Raft
({{ozone.client.datastream.putblock.without.raft.enabled}}) and datanode
streaming ({{hdds.container.ratis.datastream.enabled}}) are off by default;
HDDS-17431, HDDS-17432 and HDDS-17435 are master only and need both.
* HDDS-17430 and HDDS-17435 need a datanode that stops without a Ratis
snapshot. The reproductions emulate a crash by turning off the snapshot taken
on stop; a real process kill was not run. The replica deletion in HDDS-17435
was seen on a mini cluster with shortened SCM timeouts.
* Landing order: HDDS-17432 and HDDS-17439 depend on HDDS-17431, and the
HDDS-17439 patch applies on top of the HDDS-17431 patch. HDDS-17435 and
HDDS-17430 touch the same test class, as do HDDS-17438, HDDS-17439 and
HDDS-17431; the second one to land needs a trivial rebase.
* With the HDDS-17431 fix, a client whose stream close fails retries on a new
pipeline; while SCM still hands out pipelines with a stopped datanode, that
retry can go on for minutes. The retry behaviour predates the patch.
* The patches were built and tested on the pinned commit and apply to master at
1acf315d546 (HDDS-17439 after HDDS-17431). They are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify dn-putblock-no-raft (Apache Ozone master @7212465)
> -------------------------------------------------------------------
>
> Key: HDDS-17233
> URL: https://issues.apache.org/jira/browse/HDDS-17233
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: dn-putblock-no-raft.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
> {{dn-putblock-no-raft}}. Scope and code entry points are in the attached
> guidance file [^dn-putblock-no-raft.guidance.md]. Added after PutBlock
> without Raft on the streaming write path landed (HDDS-15757, HDDS-15758,
> HDDS-16008). HDDS-16427 and HDDS-16433 covered the write path and BCSID
> durability before this change.
> h3. Run environment
> {noformat}
> Apache Ozone commit: 7212465c0bb19615708c144238317db51c2a696d
> 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 \
> "dn-putblock-no-raft|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 ({{20d95ed}}); 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]
