[
https://issues.apache.org/jira/browse/HDDS-16475?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18125697#comment-18125697
]
Siyao Meng commented on HDDS-16475:
-----------------------------------
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: ea69b4a7d9abd040e5259dbcbb7c6ce52eb5d199
Specula: v1.2.0-24-g6190c183 with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Total: 4h 57m agent time, 102.4M tokens, about $83 (estimate)
{noformat}
h3. Result
14 candidate findings came out of model checking (7) and code review (7), and
all 14 were investigated individually. No spec repair requests were raised by
confirmation.
||Disposition||Count||
|Reproduced|11|
|Masked (defect present, harm prevented by another component today)|1|
|False positive|2|
One reproduced finding is already reported and still open (HDDS-16768). Of the
other ten, four share one root cause and one fix and are one issue, and two
more share another, which leaves six issues. Each was 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, and the fix patch,
reproduction and report were reviewed independently and reworked where the
review asked for it before filing. That validation found two more defects in
the same area, which are filed as well (HDDS-16822 and HDDS-16829).
h3. Filed
||Issue||Priority||Summary||
|HDDS-16830|Critical|Lease recovery matches open key and fileTable blocks by
count, so it can drop blocks, repeat the last block, never complete or commit a
hole|
|HDDS-16823|Critical|OMRecoverLeaseRequest calls SCM and generates block tokens
in validateAndUpdateCache, so applying RecoverLease depends on SCM|
|HDDS-16827|Major|Lease recovery commit closes the file of a writer that
overwrote the path during the recovery and drops its hsynced data|
|HDDS-16828|Major|[hsync] Datanode accepts a PutBlock on a finalized block if
it is logged after FinalizeBlock or sent through the data stream|
|HDDS-16824|Major|Lease recovery takes the block length from the first replica
it can ask, so a lagging replica truncates hsynced data|
|HDDS-16825|Major|OM closes the file of a live hsync writer at the lease hard
limit and drops data that hsync acknowledged|
|HDDS-16822|Major|Data stream hsync with PutBlock through Raft commits a block
length whose last 1MB exists only in datanode memory|
|HDDS-16829|Major|FinalizeBlock for a block the datanode does not have marks
the container UNHEALTHY and closes the pipeline|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch attached, and each except HDDS-16823 and
HDDS-16829 a standalone reproduction test.
h3. Not filed
* Already reported: after a delete, the close of the hsync writer recreates the
file on blocks that are already in {{deletedTable}}. This is HDDS-16768,
reproduced here and still open.
* Masked: the datanode leader marks a block as finalized when it sees the
FinalizeBlock request, also when that request is never committed, and then
keeps rejecting the writer. No caller gets a wrong outcome, because OM has put
the file under lease recovery before any FinalizeBlock is sent. The patch on
HDDS-16828 removes that early mark.
* False positive: the same block test in the recovery handler compares the
local ID only. SCM issues local IDs from one sequence for the whole cluster, so
this is equivalent to comparing the full block ID.
* False positive: a second FinalizeBlock is not rejected and can return a
larger length. OM accepts exactly one recovery commit for the file, so only one
length is ever published.
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 \
"ozonefs-lease-recovery|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* Every issue needs hsync, which is off by default ({{ozone.fs.hsync.enabled}}
and {{ozone.hbase.enhancements.allowed}}). HDDS-16822 and the data stream half
of HDDS-16828 also need the data stream settings, which are off by default as
well.
* All reproductions ran on single machine mini clusters, most with small block
sizes and shortened lease limits.
* HDDS-16830: the patch is client only. A file whose open key is three or more
blocks ahead of fileTable is then refused with a clear error instead of being
closed wrongly, until OM returns the pipelines of all those blocks, which
depends on HDDS-16823.
* HDDS-16827 needs another client to overwrite and hsync the file while a
recovery is between its two OM requests. The reproduction widens that window
with the datanode fault injector that {{TestLeaseRecovery}} already uses. A
stale recovery commit with an empty block list is not covered by the patch.
* HDDS-16828: the Raft path needs a writer's PutBlock to be appended to the log
after it passed the leader's check. The reproduction holds the request there
with a Ratis test hook, and 160 free running attempts during confirmation did
not hit the window. The data stream path needs no timing.
* HDDS-16824 needs a datanode that missed hsyncs while it was down to come back
before its replica is removed, and the fallback length read of the recovery to
be answered by it.
* HDDS-16825 needs a file that is kept open for longer than
{{ozone.om.lease.hard.limit}} (7d by default) and grows by less than one block
in that time. The patch covers the hard limit only, the same stale time in the
soft limit check is raised there as a question.
* HDDS-16823 and HDDS-16829 have a patch with unit tests and no standalone
reproduction.
* The patches were built and tested on the pinned commit and apply to master at
bdff9801bb2. HDDS-16822 and HDDS-16828 change the same call in
{{KeyValueHandler.handlePutBlock}}. HDDS-16828 and HDDS-16829 extend the same
condition in {{ContainerStateMachine.applyTransaction}}. HDDS-16824, HDDS-16828
and HDDS-16830 touch the same test imports in {{TestLeaseRecovery}}, as do
HDDS-16823 and HDDS-16827 in {{TestOMRecoverLeaseRequest}}. In each case the
later one to land needs a small rebase.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify ozonefs-lease-recovery (Apache Ozone master @ea69b4a)
> ----------------------------------------------------------------------
>
> Key: HDDS-16475
> URL: https://issues.apache.org/jira/browse/HDDS-16475
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: ozonefs-lease-recovery.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
> {{ozonefs-lease-recovery}}. Scope and code entry points are in the attached
> guidance file [^ozonefs-lease-recovery.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: ea69b4a7d9abd040e5259dbcbb7c6ce52eb5d199
> 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 \
> "ozonefs-lease-recovery|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
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
