[
https://issues.apache.org/jira/browse/HDDS-16541?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18126095#comment-18126095
]
Siyao Meng commented on HDDS-16541:
-----------------------------------
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: 28G memory, 8 workers
Total: 4h 38m agent time, 63.6M tokens, about $65 (estimate)
{noformat}
h3. Result
6 candidate findings came out of model checking (3) and code review (3), and
all 6 were investigated individually.
||Disposition||Count||
|Reproduced|3|
|Masked (defect present, harm prevented by another component today)|1|
|False positive|1|
|Dropped|1|
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.
h3. Filed
||Issue||Priority||Summary||
|HDDS-16900|Major|Primary SCM restart can lower the replicated CertificateId
row, so certificate IDs are returned twice|
|HDDS-16899|Major|SCM bootstrap falls back to Raft log replay when the
checkpoint download fails, so the new SCM lacks DB state that is not in the log|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch and a standalone reproduction attached.
h3. Not filed
* Masked: {{SequenceIdGenerator.getNextId}} holds the generator lock across the
Ratis call while {{notifyLeaderChanged}} takes the same lock under the Ratis
server monitor. Validation found no reachable schedule (read from the Ozone and
Ratis 3.3.1 sources, not run again): the request thread would have to stay
suspended for the whole time the SCM is a follower while the other threads run.
* False positive: a deposed leader keeps serving the rest of its local batch.
The IDs stay unique, because a batch is adopted only after the node's own
allocation has been applied.
* Dropped: reconciliation of the in memory batch, the transaction buffer and
the durable row at restart and checkpoint install. No sequence ID violation was
produced. The one residual observation concerns the checkpoint download service
after a checkpoint install and belongs to the scm-checkpoint-install target
(HDDS-16537).
* Found during validation, not a pipeline finding: {{ContainerBalancer}} saves
its state through Ratis while holding its lock, and a leader step down takes
that lock under the Ratis server monitor. Reproduced on the pinned commit. It
is the callback already reported in HDDS-16029, so no separate issue was filed.
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-sequence-id|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-16900 needs the most recently allocated certificate IDs to have no
stored certificate when the primary SCM stops, and then a restart of the
primary. The effect that was run at default settings is a bounded run of
refused certificate requests on a three SCM cluster, after which the rows are
equal again. Two stored certificates with one serial were shown only with a
certificate lifetime of 3 seconds.
* HDDS-16899 needs an SCM bootstrap whose checkpoint download fails while the
leader's Raft log still starts at index 0. Duplicate container IDs were shown
with a {{containerId}} row written directly into the DB to stand for a cluster
upgraded from SCM without Ratis. A real upgrade was not run. On a cluster that
always ran with Ratis the rows that matter converged.
* With the HDDS-16899 patch a bootstrap whose download keeps failing no longer
joins. Its start fails after the {{addSCM}} timeout (run with the timeout
lowered to 20s, the default of 15m was not run).
* {{TestSecretKeySnapshot}} and four cases of {{TestSecureOzoneCluster}} time
out in the test environment with and without the patches, so the secure cluster
paths rest on the attached reproductions, unit tests and CI.
* The run was interrupted once by a usage limit at the start of specification
validation and resumed from there.
* The patches were built and tested on the pinned commit and apply to master at
f650a22f3e3. They touch no common file.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify scm-sequence-id (Apache Ozone master @b0aa647)
> ---------------------------------------------------------------
>
> Key: HDDS-16541
> URL: https://issues.apache.org/jira/browse/HDDS-16541
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: scm-sequence-id.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-sequence-id}}. Scope and code entry points are in the attached guidance
> file [^scm-sequence-id.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-sequence-id|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]
