[
https://issues.apache.org/jira/browse/HDDS-16540?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18126105#comment-18126105
]
Siyao Meng commented on HDDS-16540:
-----------------------------------
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: 6h 13m agent time, 100.1M tokens, about $66 (estimate)
{noformat}
h3. Result
12 candidate findings came out of model checking (4) and code review (8), and
all 12 were investigated individually.
||Disposition||Count||
|Reproduced|4|
|Masked (defect present, harm prevented by another component today)|2|
|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-16896|Major|Bootstrapped SCM builds its container safe mode rules from
its empty DB and leaves safe mode before datanodes report its containers|
|HDDS-16895|Minor|SCM can leave safe mode below the container threshold when a
container report is processed during the container rule refresh|
|HDDS-16894|Minor|OneReplicaPipelineSafeModeRule still counts reports of
pipelines closed during safe mode after its refresh lowers the threshold|
|HDDS-16904|Minor|HealthyPipelineSafeModeRule keeps pipelines closed during
safe mode in its threshold, so a running SCM can stay in safe mode|
|HDDS-16903|Minor|HealthyPipelineSafeModeRule counts DORMANT and CLOSED
pipelines, so SCM can leave safe mode with no healthy OPEN RATIS/THREE pipeline|
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-16903 is a masked finding filed because the manual validation
found a way for SCM to leave safe mode with no healthy OPEN pipeline.
h3. Not filed
* Masked: the EC container rule counts reporting datanodes, not distinct
healthy replica indexes. It was reproduced only in an in process unit test, and
no consequence was found: reads of CLOSED containers are not gated by safe
mode, and every service released by the exit uses index aware replica state.
* 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-safe-mode|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-16896 was reproduced for a newly bootstrapped SCM. Its fix relies on
HDDS-14989 (2.3.0) for the order in which the datanode server starts; released
versions 2.2.0 and 2.2.1 are affected, and a backport without HDDS-14989 needs
more care. The restart case uses the same mechanism and was argued from code,
not run.
* HDDS-16895 needs a container report to be processed during a rule refresh. At
default settings the shortfall is a few percent below the cutoff, estimated
from code; the larger drop seen in testing came from shortened refresh settings.
* HDDS-16904 needs fewer than three healthy datanodes left (a minimum datanode
count of 2 or less) or safe mode pipeline creation disabled. It clears on an
SCM restart.
* HDDS-16903 and HDDS-16904 add the same two test imports, so whichever lands
second needs a trivial rebase.
* The patches were built and tested on the pinned commit and apply to master at
a5aeb764d80.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify scm-safe-mode (Apache Ozone master @b0aa647)
> -------------------------------------------------------------
>
> Key: HDDS-16540
> URL: https://issues.apache.org/jira/browse/HDDS-16540
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: scm-safe-mode.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-safe-mode}}. Scope and code entry points are in the attached guidance
> file [^scm-safe-mode.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-safe-mode|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]
