[
https://issues.apache.org/jira/browse/HDDS-17231?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18131321#comment-18131321
]
Siyao Meng commented on HDDS-17231:
-----------------------------------
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: 5f7111a27ea07ce6b7bf5284a4213ebacb65f2ae
Specula: v1.2.0-34-gcdd19e39
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 40G memory, 20 workers
Total: 4h 8m agent time, 102.8M tokens, about $48 (estimate)
{noformat}
h3. Result
10 candidate findings came out of model checking (2) and code review (8), and
all 10 were investigated individually. No spec repair requests were raised by
confirmation.
||Disposition||Count||
|Reproduced|2|
|Masked (defect present, harm prevented by another component today)|2|
|False positive|5|
|Dropped as already reported|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
(checked on 2026-10-23), and the fix patch, reproduction and report were
reviewed independently before filing. Both masked findings are filed as Minor,
since each removes a guard that the version framework relies on. The
independent reviews found two further defects in the same code, HDDS-17421 and
HDDS-17420, which went through the same validation and review.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17423|Major|SCM bootstrapped into a ring that is not finalized starts
finalized, finalizes datanodes without an admin finalize and gets them fenced|
|HDDS-17422|Major|OM bootstrapped into a pre-finalized OM ring runs at its
software version, exposes unfinalized features and stalls finalization while it
leads|
|HDDS-17421|Major|SCM terminates when it applies a Raft log entry written by
the pre-ZDU SCM finalization, and again on every restart|
|HDDS-17418|Minor|Pipeline write version uses the first datanode's version, so
writes on looked up pipelines can carry a version above the lowest member|
|HDDS-17419|Minor|OM accepts If-None-Match ETag on CreateKey and
CompleteMultipartUpload before it is finalized for S3_IF_NONE_MATCH_ETAG|
|HDDS-17420|Minor|S3 writes with an If-None-Match ETag return an unmapped HTTP
500, retried by SDKs, while OM does not support S3_IF_NONE_MATCH_ETAG|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch and a standalone reproduction test attached.
h3. Not filed
* Already reported: an SCM follower that has not applied the finalize entry
fences a finalized datanode at registration, and fencing is not checked on
heartbeats (HDDS-17090, HDDS-16798).
* False positive: within one block, the streaming calls and the PutBlock,
writeChunk and finalizeBlock calls can carry different write versions. No
datanode code reads the value.
* False positive: a datanode that loses its VERSION file restarts at a lower
apparent version while its open blocks keep the higher one. SCM repairs it in
about a second and nothing reads the stale value.
* False positive: some version comparisons use {{compareTo}} or ordinals
instead of {{isSupportedBy}}. They are equivalent at this commit.
* False positive: a request layout version stamp that is not read at apply time
and a null check that cannot fail. Neither changes applied state.
* False positive: follower reads evaluate version gates and serve the service
list at a lagging apparent version. That only ever errs low, which is safe.
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 \
"zdu-mixed-version-gating|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17423 and HDDS-17422 were reproduced on mini clusters through the normal
bootstrap commands. No older release build was available, so for HDDS-17423 the
registration of a datanode on older software was emulated by sending the
request that release builds, and for HDDS-17422 an OM on older software
applying an If-None-Match create unconditionally was argued, not run. The older
releases in their Affects Version/s were read at their tags, not run.
* HDDS-17421 needs an SCM that applies a pre-ZDU finalize entry on the new
code: one that was down or behind while its ring finalized on the old release,
or one stopped uncleanly before a snapshot covered the finalization. It was
reproduced with a single SCM ring, not with a real 2.2.x ring.
* HDDS-17418 and HDDS-17419 are masked today: no datanode code reads the write
version, and shipped clients check the OM version before they send
If-None-Match.
* The patches were built and tested on the pinned commit and apply to master at
e03ba37c41d; HDDS-17419 needs a three way merge there. No two patches change
the same main source file.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify zdu-mixed-version-gating (Apache Ozone master @5f7111a)
> ------------------------------------------------------------------------
>
> Key: HDDS-17231
> URL: https://issues.apache.org/jira/browse/HDDS-17231
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: zdu-mixed-version-gating.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
> {{zdu-mixed-version-gating}}. Scope and code entry points are in the attached
> guidance file [^zdu-mixed-version-gating.guidance.md]. Added after the Zero
> Downtime Upgrade branch (HDDS-14496) was merged. HDDS-16480 and HDDS-16549
> covered OM and SCM finalization one component at a time and left
> cross-component version gating out of scope.
> h3. Run environment
> {noformat}
> Apache Ozone commit: 5f7111a27ea07ce6b7bf5284a4213ebacb65f2ae
> 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 \
> "zdu-mixed-version-gating|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 ({{20d95ed}}); 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]
