[
https://issues.apache.org/jira/browse/HDDS-17428?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18131598#comment-18131598
]
Siyao Meng commented on HDDS-17428:
-----------------------------------
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: 69d77beff60b9106e2517c36a7a1b2cc726af568
Specula: v1.2.0-35-gf5285a2b (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, 136.6M tokens, about $86 (estimate)
{noformat}
h3. Result
14 candidate findings came out of model checking (8) and code review (6), and
all 14 were investigated individually. Two scoped spec repair rounds were run
after the first confirmation pass.
||Disposition||Count||
|Reproduced|6|
|Masked (defect present, harm prevented by another component today)|6|
|False positive|2|
Each filed 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-24), and the fix patch, the draft and the
reproduction where one is attached were reviewed independently before filing.
Two pairs of findings share a fix and are one issue each (HDDS-17443,
HDDS-17445). Three masked findings are filed: two share the fix of a reproduced
finding (part of HDDS-17443 and HDDS-17445), and one leaves a cut off frame on
a live connection (HDDS-17444).
h3. Filed
||Issue||Priority||Summary||
|HDDS-17437|Major|XceiverServerDomainSocket does not release the xceiver count
of a connection it rejects at the limit|
|HDDS-17441|Major|Interrupted short-circuit GetBlock fails with
NullPointerException and leaves the received block file stream open in
XceiverClientShortCircuit|
|HDDS-17442|Major|Domain socket requests run on the read executor shared with
gRPC, where a response write that waits for its reader holds a thread|
|HDDS-17444|Major|Domain socket Receiver keeps the connection after a response
send fails partway, so the next response follows a cut off frame|
|HDDS-17445|Major|Short-circuit GetBlock parks the opened block file in a map
shared by all requests instead of handing it to the request's own context|
|HDDS-17436|Minor|XceiverServerDomainSocket retries a failed accept() at once
and spins while the datanode is out of file descriptors|
|HDDS-17443|Minor|Domain socket Receiver logs an NPE for every response without
a block file and sends no reply to a GetBlock that is not granted access|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch attached; HDDS-17436, HDDS-17441,
HDDS-17443 and HDDS-17444 also have a standalone reproduction test, and the
others are covered by the regression tests in their patches. All seven defects
are in master only; no release contains the short-circuit read code.
h3. Not filed
* Masked: a short-circuit stream keeps reading the descriptor of a replica that
was deleted and replaced. Client checksum verification, on by default, rejects
the corrupt read; whether the client should then drop the descriptor belongs to
the client read retry work (HDDS-16545).
* Masked: a connection accepted while the server stops leaves its socket open.
In production the server stops only during datanode shutdown, and the process
exit closes it.
* Masked: a failed short-circuit block file open does not schedule a volume
check. The client's gRPC fallback read on the same datanode schedules it, and
the datanode log keeps the cause.
* False positive: a timed out response dropped while the connection stays open
never reaches a waiting client with the realistic timeout settings.
* False positive: a descriptor handed out for a container already removed
exposes exactly the bytes its BlockData describes.
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 \
"dn-short-circuit-read|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* Validation ran on macOS, not in secure mode. The CPU and log rate figures of
HDDS-17436 come from the pipeline's Linux run on unmodified code; the patch was
shown with a mocked failing accept.
* HDDS-17442 runs each domain socket request on its connection's thread, so one
connection's GetBlocks are handled one at a time. The throughput effect was not
measured.
* The wrong offset case in HDDS-17444 is from code reading; the cut off frame
was shown on a live connection, the merged message only by feeding bytes to the
client parser.
* The patches were built and tested on the pinned commit and apply to master at
1acf315d546, each on its own. HDDS-17443 and HDDS-17445 change adjacent lines
in {{Receiver.ProcessRequestTask.run}}; HDDS-17442 removes the read executor
argument that the new tests of HDDS-17436, HDDS-17437, HDDS-17441, HDDS-17443
and HDDS-17444 pass; several patches add the same test imports or helpers to
{{TestXceiverServerDomainSocket}}. Whichever lands later needs a trivial rebase.
* HDDS-17441 overlaps open PRs #11294 (HDDS-16517) and #11225 (HDDS-16335),
which rework the same client code.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify dn-short-circuit-read (Apache Ozone master @69d77be)
> ---------------------------------------------------------------------
>
> Key: HDDS-17428
> URL: https://issues.apache.org/jira/browse/HDDS-17428
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: dn-short-circuit-read.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
> {{dn-short-circuit-read}}. Scope and code entry points are in the attached
> guidance file [^dn-short-circuit-read.guidance.md]. Added for the datanode
> side of short-circuit read, merged from branch HDDS-10685 after the original
> catalog was pinned. HDDS-16545 looked at the client read retry on this path
> by code reading only, because domain sockets need native libhadoop on Linux.
> h3. Run environment
> {noformat}
> Apache Ozone commit: 69d77beff60b9106e2517c36a7a1b2cc726af568
> 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 \
> "dn-short-circuit-read|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
> * 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]