[ 
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]

Reply via email to