[
https://issues.apache.org/jira/browse/HDDS-16544?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18126815#comment-18126815
]
Siyao Meng commented on HDDS-16544:
-----------------------------------
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: 031e76aa2c9a60b67185390b5b33499cbbb82e43
Specula: v1.2.0 plus 27 commits (0263f82a), with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 2h 33m agent time, 48.2M tokens, about $44 (estimate)
{noformat}
h3. Result
5 candidate findings came out of model checking (2) and code review (3), and
all 5 were investigated individually.
||Disposition||Count||
|Reproduced|4|
|False positive|1|
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-10-13), and the fix patch, reproduction and report were
reviewed independently before filing.
That validation and review also found defects in the neighbouring Ratis key
write path ({{KeyOutputStream}}), which is outside the model. They are not
pipeline findings and are not in the counts above. Each went through the same
validation and independent review and is filed below.
h3. Filed
>From the verification run:
||Issue||Priority||Summary||
|HDDS-16974|Major|EC file checksum is not bounded by the committed block group
length when a replica lists a stripe beyond it|
|HDDS-16973|Major|ECKeyOutputStream.close() does not end its flush thread after
a failed or cancelled write, so the thread or datanode client references stay
behind|
|HDDS-16972|Minor|EC key write fails with NullPointerException instead of
retrying the stripe when a datanode client cannot be acquired for a new block
group|
Found during validation and review, Ratis key write path:
||Issue||Priority||Summary||
|HDDS-16980|Critical|Concurrent hsync on a Ratis key returns normally after the
stream failed, and replaces the key's block list in OM with an empty one|
|HDDS-16979|Major|hsync or flush on a Ratis key never returns when the block
that takes over a failed block's data fails as well|
|HDDS-16981|Major|Ratis key write waits for its own retry handling when the
data written on retry fills the replacement block|
|HDDS-16975|Minor|Ratis key write fails with NullPointerException and hides the
real error when a block output stream cannot be created|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch attached. HDDS-16974 and HDDS-16981 have no
standalone reproduction attached, the regression test in the patch covers them.
The others have a standalone reproduction test.
h3. Not filed
* False positive: EC PutBlock has no ordering guard on the datanode, so a stale
PutBlock applied after a newer one would shrink the replica metadata. No real
call sequence was found that delivers a stale PutBlock again.
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-ec-write|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-16974 was reached on a mini cluster by stopping one datanode between two
stripes of a key write.
* HDDS-16973 needs the application to cancel the thread that is in {{write()}}
or {{close()}}. Nothing in Ozone's own code was found to do that. The
reproductions use mock OM and datanode clients, nothing was run against a real
cluster.
* HDDS-16972 was triggered for real only with
{{hdds.datanode.use.datanode.hostname=true}} and a datanode hostname that is
not a valid URI host. No node specific trigger was found in the default
configuration.
* HDDS-16980 and HDDS-16979 need concurrent calls on one key stream
({{ozone.client.hbase.enhancements.allowed=true}} and a write concurrency other
than 1), which is the HBase configuration. Both were run with mock datanodes
and on a mini cluster with client side error injection. Neither was run with
HBase or with a real datanode outage.
* HDDS-16981 needs {{ozone.scm.block.size}} at or below
{{ozone.client.stream.buffer.max.size}} (defaults 256MB and 32MB), so the
default block size is not affected. It was run with mock datanodes and on a
mini cluster.
* HDDS-16975 was only triggered by client side configuration errors, such as an
unsupported value of {{hdds.ratis.client.request.watch.type}}.
* The patches were built and tested on the pinned commit. All of them apply to
master at d0454e0cffd. HDDS-16972 and HDDS-16973 change the same import block
of {{TestOzoneECClient}}, HDDS-16979 and HDDS-16980 both add a test to
{{TestKeyOutputStream}}, and HDDS-16975 and HDDS-16981 both add a test to
{{TestOzoneClient}}, so in each pair the second one to land needs a rebase of
that test file. All other pairs apply on top of each other.
* The patch of HDDS-16980 was narrowed after its independent review so that a
call racing a normal {{close()}} keeps its behaviour. That last revision was
tested again but not reviewed independently a second time.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify client-ec-write (Apache Ozone master @031e76a)
> ---------------------------------------------------------------
>
> Key: HDDS-16544
> URL: https://issues.apache.org/jira/browse/HDDS-16544
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: client-ec-write.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-ec-write}}. Scope and code entry points are in the attached guidance
> file [^client-ec-write.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: 031e76aa2c9a60b67185390b5b33499cbbb82e43
> 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-ec-write|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]
