[
https://issues.apache.org/jira/browse/HDDS-16538?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18126108#comment-18126108
]
Siyao Meng commented on HDDS-16538:
-----------------------------------
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: 7h 17m agent time, 124.2M tokens, about $77 (estimate)
{noformat}
h3. Result
13 candidate findings came out of model checking (7) and code review (6), and
all 13 were investigated individually.
||Disposition||Count||
|Reproduced|4|
|Masked (defect present, harm prevented by another component today)|5|
|False positive|3|
|Dropped (already reported upstream)|1|
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-16889|Minor|Admin pipeline activate reopens a CLOSED pipeline, and
deactivate moves a CLOSED or ALLOCATED pipeline to DORMANT|
|HDDS-16905|Minor|SCM keeps deleted pipelines in its datanode to pipeline map
after a Ratis snapshot install, so decommission and maintenance stall while it
is leader|
|HDDS-16906|Minor|Pipeline with a DEAD datanode stays OPEN if SCM leadership
changes while the node goes STALE and DEAD, and its EC container is not
repaired|
|HDDS-16890|Minor|SCM closePipeline leaves a container allocated during the
close OPEN on the CLOSED pipeline until the pipeline is deleted|
|HDDS-16888|Minor|Pipeline scrubber closes and deletes a pipeline that was
opened after the scrubber read it as a timed out ALLOCATED pipeline|
|HDDS-16887|Minor|Pipeline scrubber pass stops at a pipeline removed by another
thread and skips the remaining pipelines until the next pass|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch and a standalone reproduction test
attached. HDDS-16890, HDDS-16888 and HDDS-16887 are masked findings filed
because the manual validation found the harm reachable or the repair
incomplete; HDDS-16890 also covers the block allocation and ReplicationManager
variants of the same close race.
h3. Not filed separately
* Reproduced: the safe mode healthy pipeline rule counts DORMANT and CLOSED
pipelines. It is the same defect found by the safe mode run and is filed there
as HDDS-16903.
* Dropped: one finding duplicates HDDS-16453.
* The three false positives were judged not to hold on a running SCM: invariant
artifacts of the model, an admin delete the RPC interface does not expose, and
a rollback no reachable fault runs.
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-pipeline-lifecycle|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-16889 is reachable only through the admin activate and deactivate
commands, and a close the datanode asked for is resent within one heartbeat.
The EC variant was not run.
* HDDS-16905 needs Ratis log purge, which is off by default, and a follower
that falls behind a purge and later becomes leader. The reproduction shrank the
purge gap.
* HDDS-16906 needs two leader changes, each within a few seconds of a node
state change. The reproduction held the window open with an existing health
check pause hook.
* HDDS-16890 and HDDS-16888: client side retry and client visible impact were
argued from code, not exercised.
* HDDS-16887, HDDS-16888 and HDDS-16906 all change the scrubber loop. Land
HDDS-16887 first; the other two then need a trivial rebase.
* HDDS-16905 has a one line textual overlap with apache/ozone#11349.
* The patches were built and tested on the pinned commit and apply to master at
b9b33851b20.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify scm-pipeline-lifecycle (Apache Ozone master @b0aa647)
> ----------------------------------------------------------------------
>
> Key: HDDS-16538
> URL: https://issues.apache.org/jira/browse/HDDS-16538
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: scm-pipeline-lifecycle.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-pipeline-lifecycle}}. Scope and code entry points are in the attached
> guidance file [^scm-pipeline-lifecycle.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-pipeline-lifecycle|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]
