[
https://issues.apache.org/jira/browse/HDDS-16579?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18130993#comment-18130993
]
Siyao Meng commented on HDDS-16579:
-----------------------------------
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: 9c3e5477ffb9f41da639051aaa5e9d7bd8b53fe4
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 52m agent time, 46.6M tokens, about $41 (estimate)
{noformat}
h3. Result
10 candidate findings came out of model checking (5) and code review (5), and
all 10 were investigated individually. No spec repair requests were raised by
confirmation.
||Disposition||Count||
|Reproduced|5|
|Masked (defect present, harm prevented by another component today)|2|
|False positive|3|
Four findings (two reproduced, two masked) share one fix, so they are one
issue. 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-23), and the fix patch, reproduction and
report were reviewed independently before filing. One more defect was found
during that review and is filed as well (HDDS-17396).
h3. Filed
||Issue||Priority||Summary||
|HDDS-17395|Major|Restarted BackgroundService can stop for good or run batches
from its old executor after a forced shutdown|
|HDDS-17394|Minor|Registering a reconfiguration callback while a
reconfiguration is completing skips the remaining callbacks and the status
listener|
|HDDS-17396|Minor|BackgroundService.start on a running service schedules a
second loop, which can deadlock a new DirectoryDeletingService started by a
reconfiguration|
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
* Reproduced: an owner stop while a reconfiguration restart of
DirectoryDeletingService is in flight revives the service after its owner
stopped it. Same owner, end state and fix as HDDS-17296, whose attached patch
also closes this window (run).
* Reproduced: after a reconfiguration restart rejects a
DirectoryDeletingService round before it is submitted, the next round publishes
it as completed with zero directories. One interval of wrong gauges, cumulative
counters stay correct, and the window is a few microseconds; too small for an
issue of its own.
* False positive: {{BackgroundService.start}} has no guard against a second
call. The pipeline found no production caller; the review found one, so it is
covered by HDDS-17396.
* False positive: an exception from {{getTasks}} or {{execTaskCompletion}}
cancels the periodic task. No trigger found other than JVM wide heap exhaustion.
* False positive: reconfiguration restart callbacks hold the reconfiguration
lock for up to 60 to 120 s. Status and start requests are delayed but return
correct results.
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 \
"background-service|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* All three issues need an admin reconfiguration ({{ozone admin reconfig ...
start}}) of a deleting service's interval, timeout or worker count. HDDS-17395
additionally needs a batch whose tasks have not all started when the 60 s
shutdown wait of the restart runs out; on a datanode with a deletion backlog
that is plausible (argued from the code, not measured). The reproductions use
real timeouts and a held task.
* HDDS-17394 and HDDS-17396 also need the reconfiguration to coincide with a
checkpoint install on an OM follower (HDDS-17396 also applies to a datanode
reconfigured before its first SCM handshake, from code reading). The
reproductions use a stand-in callback or call {{updateAndRestart}} directly; a
real reconfiguration during a real install was not exercised.
* The patches were built and tested on the pinned commit and apply to master at
c521a16af75. HDDS-17395 and HDDS-17396 change the same line of
{{BackgroundService.start}}, so the second one to land needs a one line rebase;
both applied together pass {{TestBackgroundService}} and
{{TestDirectoryDeletingService}}.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify background-service (Apache Ozone master @9c3e547)
> ------------------------------------------------------------------
>
> Key: HDDS-16579
> URL: https://issues.apache.org/jira/browse/HDDS-16579
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: background-service.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
> {{background-service}}. Scope and code entry points are in the attached
> guidance file [^background-service.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: 9c3e5477ffb9f41da639051aaa5e9d7bd8b53fe4
> 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 \
> "background-service|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]
