[
https://issues.apache.org/jira/browse/HDDS-17642?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18136785#comment-18136785
]
Siyao Meng commented on HDDS-17642:
-----------------------------------
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.2.0-35-gf5285a2b with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context), on a lab host on the
Claude subscription
Effort: medium
TLC limits: 40G memory, 20 workers
Total: 11h 19m agent time, 227.6M tokens, about $125 (estimate)
{noformat}
h3. Result
18 candidate findings came out of model checking (4) and code review (14), and
all 18 were investigated individually. Two model checking findings were traced
to the model and led to one round of spec repair (they are counted as false
positives below); the other two still held against the repaired spec.
||Disposition||Count||
|Reproduced|5|
|Masked (defect present, harm prevented by another component today)|5|
|False positive|8|
Each reproduced finding and two of the masked ones were 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,
reproduction and report were reviewed independently before filing. The reviews
widened two fixes (HDDS-17674 now also reports the failure to SCM, HDDS-17677
also covers CLOSING containers).
h3. Filed
||Issue||Priority||Summary||
|HDDS-17675|Major|Datanode acknowledges and commits a WriteChunk without
writing its data when a truncated entry at the same log index still has a
pending write|
|HDDS-17678|Major|PutBlock piggybacked on WriteChunk does not update the BCSID
saved in the Ratis snapshot, so the restart check misses its loss|
|HDDS-17674|Major|Datanode closes the Raft division on the Ratis thread that
called write(), so after a write timeout the close hangs and the replica stays
CLOSING|
|HDDS-17673|Minor|WriteChunk appended after its container's CloseContainer
commits with no data on the leader, so a lagging follower makes it close the
pipeline|
|HDDS-17677|Minor|FILE_PER_BLOCK container bytes used is saved too low after a
datanode restart between data write and apply|
|HDDS-17676|Minor|FinalizeBlock lowers the stored block bcsId to the request's
when the block has no last_chunk_info row|
|HDDS-17672|Minor|KeyValueContainer.update clears all container metadata
instead of restoring it when the .container file rewrite fails|
Priorities follow the manual validation, not the pipeline's severity classes.
HDDS-17676 and HDDS-17672 are masked findings filed because their fixes are
small and the code contradicts its intent. Every issue has a standalone
reproduction test attached, and every issue except HDDS-17673 has a proposed
fix patch.
h3. Not filed
* Masked: a data stage result that is tolerated acknowledges a WriteChunk with
no bytes and relies on an UNHEALTHY mark that is only in memory when the
container file rewrite fails. The harm needs a second disk fault plus a restart
before the group is removed, affects only a block no client was told was
committed, and the container scanner reports it.
* Masked: a thrown apply failure does not ask SCM to close the pipeline at
once, unlike a returned one. Reached only through a mocked dispatcher, and the
next entry or WriteChunk on the pipeline closes it anyway.
* Masked: {{ContainerController}} quasi close and close do not check for a
removed container. Needs a container removed during group removal, and SCM's
repeated close commands quasi close the containers that were skipped.
* False positive: a PutBlock apply after a group removal quasi close. The model
allowed the snapshot and the quasi close before all submitted applies finished,
which Ratis does not; the spec was repaired.
* False positive: a log entry durable without its chunk data. Ratis waits for
the data write before it writes the entry; the spec was repaired.
* False positive: queued chunk writes cancelled by the write timeout. Each sits
behind a running write that Ratis waits on in log order, so a flush never
reports it.
* False positive: {{triggerPipelineClose}} without a null check after group
removal. The action is dropped either way; robustness only.
* False positive: the volume full check rejecting a committed PutBlock on one
replica. It is fenced end to end (state machine unhealthy, pipeline closed);
availability only.
* False positive: {{closeContainer}} returning after its lock retries run out.
The only caller that holds the lock never moves OPEN or CLOSING containers.
* False positive: {{KeyValueContainer.close}} clearing the finalized block set
before it changes state. No reader is affected.
* False positive: quasi close failures on group removal logged at DEBUG.
Diagnostics only.
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 \
"dn-container-apply|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17675 needs a leadership loss while the old leader's volume is slow. The
reproduction drives the real state machine and Ratis log in one process with
one chunk executor held busy. The variant for entries received as a follower is
argued from the code, not run.
* HDDS-17678 needs the two client settings that enable piggybacking and a power
loss. The reproduction simulates the lost write by resetting the persisted
BCSID; no real power loss was run.
* HDDS-17674 affects master only (introduced by HDDS-15443). The reproduction
shortens the write wait interval to stand in for a stalled disk. The one day
bound comes from reading the Ratis code. The patch runs the close on the common
pool; a dedicated executor is the alternative named in the issue.
* HDDS-17673 needs two timing windows and a lagging follower; the reproduction
uses a Ratis test hook. Its fix needs RATIS-2722 (Ratis 3.4.0, not released
yet), so no patch is attached.
* HDDS-17677 was reproduced with the restart simulated in one process.
* HDDS-17676 affects master only (a follow up to HDDS-16730); no current reader
presents the higher bcsId. HDDS-17672 has no current caller, since no Ozone
code sends UpdateContainer today.
* The patches were built and tested on the pinned commit and apply to master at
7294fc2da18. HDDS-17675 and HDDS-17674 both change {{ContainerStateMachine}}
and {{ContainerStateMachineTests}}; the second one to land needs a trivial
rebase of the test file.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify dn-container-apply (Apache Ozone master @ec5ed5f)
> ------------------------------------------------------------------
>
> Key: HDDS-17642
> URL: https://issues.apache.org/jira/browse/HDDS-17642
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: dn-container-apply.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-container-apply}}. Scope and code entry points are in the attached
> guidance file [^dn-container-apply.guidance.md]. Added as a narrower rerun of
> dn-container-state-machine (HDDS-16433), which modeled BCSID durability, the
> container snapshot and ordered apply at 9fbf9ee and filed only an
> unreproduced finding; this one adds write timeouts, failure results treated
> as success, close paths outside Raft and lagging followers.
> 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 \
> "dn-container-apply|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]
