[
https://issues.apache.org/jira/browse/HDDS-16539?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18125971#comment-18125971
]
Siyao Meng commented on HDDS-16539:
-----------------------------------
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: b0aa6475b7856d2c7f467dd3db12b9a1dd116f63
Specula: v1.0.0-56-g62f63a1e (with local changes)
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 40G memory, 20 workers
Total: 4h 18m agent time, 101.2M tokens, about $65 (estimate)
{noformat}
h3. Result
14 candidate findings came out of model checking (10) and code review (4), and
all 14 were investigated individually.
||Disposition||Count||
|Reproduced|4|
|Masked (defect present, harm prevented by another component today)|4|
|False positive|6|
Each reproduced finding 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-11), and the fix patch, reproduction and
report were reviewed independently before filing.
h3. Filed
||Issue||Priority||Summary||
|HDDS-16893|Major|SCM can grant a datanode's container slot again after the ICR
of a new container, until the datanode's next node report|
|HDDS-16892|Minor|SCM drops the pending container allocations of a datanode
that re-registers with a new version or port set, so its last slot can be
granted twice|
|HDDS-16891|Minor|After an SCM restart or leader change, SCM has no pending
container allocations and grants again the slots reserved for containers not
yet written|
Priorities follow the manual validation, not the pipeline's severity classes.
HDDS-16893 and HDDS-16892 have a proposed fix patch and a standalone
reproduction test attached. HDDS-16891 is a design limitation: it has a
reproduction and a proposed design (rebuild the reservations once the new
leader is ready), no patch.
h3. Not filed
* Reproduced: a stale incremental container report redelivered after a lost
heartbeat response completes a later replication ADD to the same datanode. The
trigger needs the heartbeat to fail after SCM processed it plus an ADD of the
same container within about one heartbeat, the harm is limited by the datanode
import space check, and a real fix needs a protocol change.
* Masked: a replication reservation can age out while the command is still
queued. The datanode spare space band and its own space check absorb the double
grant today, and the right reservation lifetime is a design question.
* Masked: a late window roll and a re-scheduled replication counted in both
windows can make a datanode look full when it is not. Both only err on the
conservative side, clear at the next roll, and do not occur with the default
metrics sampling and replication timeout.
* Masked: a failed replicated {{addContainer}} keeps its reservation until the
window ages out. Releasing it is unsafe because the request may still commit;
it is discussed in HDDS-16891, whose proposed rebuild also clears it.
* The six false positives were judged not to hold on a running SCM: invariant
artifacts of the model, unreachable orderings, or intended behaviour.
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=40G --tlc-worker-limit=20 \
"scm-pending-allocation|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-16893 was reproduced with real SCM components and the datanode's own
space check, with default settings. The Ratis pipeline close that follows the
failed container create was read from code, not run.
* HDDS-16892 was reproduced for a version change through public SCM entry
points. A port change takes the same code path; an address change is already
made harmless by stale pipeline closing.
* HDDS-16891 was reproduced with a leader transfer on a 3 SCM mini cluster. The
SCM restart case follows from the same code path and was not run.
* All three issues are present in 2.2.0 and 2.2.1.
* The HDDS-16892 patch conflicts textually with apache/ozone#11349 on the
{{DatanodeInfo}} constructor.
* The patches were built and tested on the pinned commit and apply to master at
6818707698c.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify scm-pending-allocation (Apache Ozone master @b0aa647)
> ----------------------------------------------------------------------
>
> Key: HDDS-16539
> URL: https://issues.apache.org/jira/browse/HDDS-16539
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: scm-pending-allocation.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
> {{scm-pending-allocation}}. Scope and code entry points are in the attached
> guidance file [^scm-pending-allocation.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: b0aa6475b7856d2c7f467dd3db12b9a1dd116f63
> 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 \
> "scm-pending-allocation|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]
