[
https://issues.apache.org/jira/browse/HDDS-17541?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18134665#comment-18134665
]
Siyao Meng commented on HDDS-17541:
-----------------------------------
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: 424482eb9cfc4b835e1bf73bcdaa9e7d70df59f0
Ratis: 3.3.1
Specula: v1.2.0 (with local changes)
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 9h 45m agent time, 204.2M tokens, about $98 (estimate)
{noformat}
h3. Result
8 candidate findings came out of model checking (4) and code review (4), and
all 8 were investigated individually.
||Disposition||Count||
|Reproduced|6|
|Environment limited (part of the chain shown, the rest argued)|1|
|Dropped (duplicate of an open issue)|1|
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, and
the patch, reproduction and report were reviewed independently before filing.
The environment limited finding was confirmed in that validation (the hang with
real OM classes, the late commit on unmodified Ratis) and is filed as well.
Several findings were narrowed in validation; the issues describe only the
parts that hold.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17579|Major|New OM leader reports ready while previous term entries are
still unapplied, so default reads miss acknowledged writes|
|HDDS-17578|Major|OM whose Ratis log write fails keeps running without ever
catching up or exiting, because it ignores notifyLogFailed|
|HDDS-17573|Major|OM follower that finishes a checkpoint install is never
reloaded by Ratis when appends it accepted earlier reach its log after the
notification|
|HDDS-17574|Major|Ratis snapshot taken while an OM checkpoint install has
paused the state machine can block the follower's apply thread forever|
|HDDS-17575|Minor|SCM that steps down while notifyLeaderReady runs stays leader
ready as a follower and is already ready when it is elected again|
|HDDS-17576|Minor|Follower SCM stops applying the Raft log until restart after
an install snapshot notification from a leader missing from its peer list|
|HDDS-17577|Minor|ozone admin om transfer -r can choose a listener OM as the
target and fail with "not in FOLLOWER role"|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a standalone reproduction test attached, and all but HDDS-17573
have a proposed fix patch.
h3. Not filed
* Dropped: the datanode {{notifyInstallSnapshotFromLeader}} reporting a
snapshot it never installed is HDDS-11720 (open).
* Parts of filed findings that did not hold: the datanode parts of the log
failure finding (closing only the pipeline is by design, the possible null
dereference has no trigger), and the priority reset parts of the leader
transfer finding (refuted, not reproduced, or already HDDS-16833).
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 \
"ratis-statemachine-contract|apache/ozone|Java|Use the target-specific
guidance"
{code}
h3. Caveats
* HDDS-17579: the reproductions hold the new leader's apply backlog with a
bucket lock (leader change) or pause the double buffer before a stop (restart);
a natural backlog was seen in the restart case. With the patch a leader with a
backlog also rejects writes until it is applied. The patch also closes the
window of HDDS-16795.
* HDDS-17573: the fix belongs in Ratis, so no Ozone patch is attached. The
reproduction runs three unmodified Ratis 3.3.1 servers with a state machine
that follows OM's install contract; the OM level effect is argued from the
code. Turning append compose off kept the window from opening in the
reproduction, which is relevant to the open PR for HDDS-14874.
* HDDS-17574: the late commit was run on Ratis and the hang with real OM
classes, but the whole chain was not driven in an OM cluster; that Ratis takes
the snapshot during OM's pause is argued from code.
* HDDS-17575: without an injected delay the race window is narrow (not hit in 5
runs).
* HDDS-17576 needs {{ozone.scm.ha.ratis.log.purge.enabled=true}} (default
false). Its patch touches the same line as the open PR for HDDS-17205, so the
second one to land needs a one line rebase.
* HDDS-17578: a failed follower always ends up stuck; a failed leader sometimes
exits on its own first.
* The patches were built and tested on the pinned commit and apply to master at
fef9cde752a. The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify ratis-statemachine-contract (Apache Ozone master @424482e)
> ---------------------------------------------------------------------------
>
> Key: HDDS-17541
> URL: https://issues.apache.org/jira/browse/HDDS-17541
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: ratis-statemachine-contract.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
> {{ratis-statemachine-contract}}. Scope and code entry points are in the
> attached guidance file [^ratis-statemachine-contract.guidance.md]. Added
> because earlier targets treated Ratis as an oracle, so mismatches between
> what Ozone's state machines assume and what Ratis 3.3.1 does were found only
> incidentally (for example in HDDS-16477). It covers the callback contract
> across OM, SCM and the datanode, not Raft itself.
> h3. Run environment
> {noformat}
> Apache Ozone commit: 424482eb9cfc4b835e1bf73bcdaa9e7d70df59f0
> 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 \
> "ratis-statemachine-contract|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 ({{efe0c7e}}); 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
(v10.3.26#10030026)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
