[
https://issues.apache.org/jira/browse/HDDS-16542?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18126202#comment-18126202
]
Siyao Meng commented on HDDS-16542:
-----------------------------------
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
Challenger debate, and severity classification.
h3. Run environment
{noformat}
Ozone commit: b9b33851b20fa11baf4b07982de9afb8ea44f85a
Specula: v1.2.0-25-g62f63a1e with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 5h 23m agent time, 84.0M tokens, about $67 (estimate)
{noformat}
h3. Result
7 candidate findings came out of model checking (6) and code review (1), and
all 7 were investigated individually. No spec repair requests were raised by
confirmation.
||Disposition||Count||
|Reproduced|7|
|Masked, false positive, dropped|0|
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-11), and the fix patch, reproduction and report were
reviewed independently before filing. Two more defects were found during that
validation and are filed as well (HDDS-16911 and HDDS-16936).
h3. Filed
||Issue||Priority||Summary||
|HDDS-16912|Major|Leader loss between root CA rotation commit and committed
leaves the rotation unfinished, and the next rotation stops every SCM|
|HDDS-16913|Major|SCM that applies a root CA rotation commit after a restart or
without a staged sub CA certificate breaks its sub CA directory and cannot
start|
|HDDS-16914|Major|SCM leader counts root CA rotation prepare acks per
certificate, so one SCM acking twice lets it commit before every SCM prepared|
|HDDS-16915|Major|SCM follower that installs a checkpoint taken after a root CA
rotation commit stays on the old root certificate|
|HDDS-16916|Major|New SCM leader blocks its Ratis log applying thread and
terminates when the root CA post-processing state is stale|
|HDDS-16917|Minor|SCM that crashes while it applies a root CA rotation commit
cannot start again, the sub CA directory switch is not completed on start|
|HDDS-16911|Minor|SCM hangs half stopped instead of exiting when a step of the
root CA rotation commit fails|
|HDDS-16936|Major|SCM issues SCM role certificates without the SCM admin check
and copies the CA basic constraint for every role|
Priorities follow the manual validation, not the pipeline's severity classes
(one Critical and six High). Each issue has a proposed fix patch and a
standalone reproduction test attached, except HDDS-16936, which has the patch
with its regression tests only.
h3. Not filed
* The code review finding had three parts. Only the blocking replicated call at
leader ready is filed (HDDS-16916). A leader step down that cancels the
rotation tasks without cleanup is transient and cleaned up by the next rotation
attempt, and the unchecked interrupt state has no reachable consequence.
* The late join variant of HDDS-16913 (an SCM added to the ring after a
rotation) is described in that issue as argued, not run.
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 \
"scm-root-ca-rotation|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* Every issue except HDDS-16936 needs secure mode, SCM HA and
{{hdds.x509.ca.rotation.enabled=true}}, which is off by default, and a rotation
runs about once per root certificate lifetime. HDDS-16915 also needs
{{ozone.scm.ha.ratis.log.purge.enabled=true}}, off by default too.
* Each of their triggers is a fault at a particular point of one rotation or
shortly after it: a leader change (HDDS-16912, HDDS-16916), a restart or kill
of an SCM after its prepare ack (HDDS-16913, HDDS-16914), a kill between two
directory moves (HDDS-16917), a follower cut off until the leader has purged
its log (HDDS-16915). The issues state the size of each window.
* What ran where: HDDS-16912, HDDS-16915 and HDDS-16916 were reproduced on a
secure mini cluster with three SCMs and were also run there with the fix.
HDDS-16913 and HDDS-16914 were seen by the pipeline on a three SCM compose
cluster built from unmodified source; their fixes were tested at unit level
only. HDDS-16917 was run against the real {{StorageContainerManager}}
constructor, not with a real kill. HDDS-16911 was run on one SCM without
security. No datanode or OM was run against any of the resulting states.
* The fixes of HDDS-16913 and HDDS-16916 were changed after their independent
review, in the direction the reviews asked for. Those changes were checked
again but not by a second reviewer.
* The patches were built and tested on the pinned commit and apply to master at
5108acff480 (HDDS-16936 was checked at 084c60d4fb9). Each is made against the
pinned commit alone. The rotation patches change the same two classes
({{RootCARotationHandlerImpl}} and {{RootCARotationManager}}) and mostly the
same unit test, so they need a manual merge when more than one lands.
HDDS-16911 and HDDS-16912 change the same three lines.
* HDDS-16913 and HDDS-16915 leave the affected SCM running but not rotated in
the cases their patches cannot complete. Both issues say so and list what
follows.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify scm-root-ca-rotation (Apache Ozone master @b9b3385)
> --------------------------------------------------------------------
>
> Key: HDDS-16542
> URL: https://issues.apache.org/jira/browse/HDDS-16542
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: scm-root-ca-rotation.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-root-ca-rotation}}. Scope and code entry points are in the attached
> guidance file [^scm-root-ca-rotation.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: b9b33851b20fa11baf4b07982de9afb8ea44f85a
> 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-root-ca-rotation|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]
