[
https://issues.apache.org/jira/browse/HDDS-16577?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18130709#comment-18130709
]
Siyao Meng commented on HDDS-16577:
-----------------------------------
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: 5fed99dab3c3204cd7bf1516074969a38d5eb00d
Specula: v1.2.0-34-gcdd19e39 with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 1h 47m agent time, 25.1M tokens, about $22 (estimate)
{noformat}
h3. Result
6 candidate findings came out of model checking (3) and code review (3), and
all 6 were investigated individually. Confirmation raised no spec repairs.
||Disposition||Count||
|Reproduced|3|
|Masked (defect present, harm prevented by another component today)|2|
|False positive|1|
Each finding 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-22), and the fix patch and report were reviewed
independently before filing. Both masked findings were filed as well: one has a
small but real effect on its own, and the other's mask (checksum verification
on read) does not cover data stored without checksums. One more defect, in the
block file write cache next to the code under verification, was found during
validation and is filed too.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17369|Major|Mapped chunk read that fails on a later piece releases the
quota of earlier pieces a second time, raising the effective mmap limit until
restart|
|HDDS-17370|Major|MappedBufferManager hands out the cached mapped buffer
itself, so a consumer that changes its position and limit corrupts the cached
entry|
|HDDS-17371|Major|Datanode mmap read cache is keyed by path only, so a
container replica recreated at the same path can be served the deleted
replica's bytes|
|HDDS-17368|Minor|MappedBufferManager loses one mmap quota permit each time a
chunk range is re-read after GC cleared its cached mapping|
|HDDS-17367|Minor|MappedBufferManager cleanup returns quota of the other chunk
layout's cached mappings because the mapping map is static|
|HDDS-17372|Minor|Datanode keeps writing to the open block file of a deleted
container replica after the replica is recreated at the same path (found during
validation)|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch attached. HDDS-17369 and HDDS-17370 have no
standalone reproduction; the regression test in the patch covers them. The
other four also have a standalone reproduction test attached.
h3. Not filed
* False positive: a read could rethrow an empty exception holder. The only
supplier sets the holder before it returns null, and the map call either yields
a buffer or throws.
h3. Reproduce
{noformat}
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-mapped-buffer|apache/ozone|Java|Use the target-specific guidance"
{noformat}
h3. Caveats
* The five mapped read issues need mapped reads to be on
({{ozone.chunk.read.mapped.buffer.max.count}} > 0, default 0) and a read whose
buffer capacity is above {{ozone.chunk.read.mapped.buffer.threshold}} (32KB),
which data written with the default 16KB per checksum does not reach.
Deployments with default settings are not affected.
* HDDS-17370 also needs {{ozone.UnsafeByteOperations.enabled=false}}.
HDDS-17367 needs a datanode that still holds FILE_PER_CHUNK containers.
* HDDS-17371 and HDDS-17372 need SCM to delete a replica and create it again on
the same volume, within one GC window and within the 10 minute write cache
expiry respectively. Both were run at the datanode level only, not with a real
EC reconstruction, replication or reconciliation.
* Everything was run on macOS in unit and datanode level tests; no mini cluster
suite turns on mapped reads.
* The patches were built and tested on the pinned commit and apply to master at
76b5c6947a2. HDDS-17367, HDDS-17368 and HDDS-17370 change the same test imports
in {{TestMappedBufferManager}} (HDDS-17368 and HDDS-17370 also both add a test
at the end of the class), and HDDS-17369 and HDDS-17371 change adjacent lines
of {{ChunkUtils.readData}}, so whichever lands later needs a trivial rebase.
HDDS-17372 overlaps the same way with the open apache/ozone#11668 and
apache/ozone#11678.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify dn-mapped-buffer (Apache Ozone master @5fed99d)
> ----------------------------------------------------------------
>
> Key: HDDS-16577
> URL: https://issues.apache.org/jira/browse/HDDS-16577
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: dn-mapped-buffer.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-mapped-buffer}}. Scope and code entry points are in the attached
> guidance file [^dn-mapped-buffer.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: 5fed99dab3c3204cd7bf1516074969a38d5eb00d
> 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-mapped-buffer|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
(v10.3.26#10030026)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
