[
https://issues.apache.org/jira/browse/HDDS-16580?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18131194#comment-18131194
]
Siyao Meng commented on HDDS-16580:
-----------------------------------
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: f804bf26867246067017fdd9e5319c2cbdbd5db8
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 28m agent time, 28.0M tokens, about $24 (estimate)
{noformat}
h3. Result
6 candidate findings came out of model checking (4) and code review (2), and
all 6 were investigated individually. No spec repair requests were raised by
confirmation.
||Disposition||Count||
|Reproduced|1|
|Masked (defect present, harm prevented by how SCM uses the LeaseManager
today)|4|
|False positive|1|
The five live findings were validated a second time by hand against the pinned
commit: a regression test was added to {{TestLeaseManager}} 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. Findings that share one fix are one
issue, so the five became three.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17404|Minor|LeaseManager monitor can expire a lease that was re-acquired
or renewed after it found the old deadline passed|
|HDDS-17403|Minor|LeaseManager.shutdown can leave a live lease when acquire
runs concurrently, and can run a lease callback after it returns|
|HDDS-17402|Minor|LeaseManager stops expiring leases for good after one
unexpected error in its monitor thread, because the restart calls start() on
the dead thread|
Priorities follow the manual validation, not the pipeline's severity classes
(which rated four of the five findings High). All three are defects of the
public LeaseManager API with no production trigger found at this commit: SCM's
{{CloseContainerEventHandler}} only acquires, nothing in main code calls
{{Lease.renew}} or releases and re-acquires a lease, and SCM closes its event
queue before shutting down the lease manager. Each issue has a proposed fix
patch and a standalone reproduction test attached.
h3. Not filed
* False positive: calling {{start()}} twice on one LeaseManager would start a
second monitor. No caller does that.
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 \
"lease-manager|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17404 and HDDS-17403 are races. Their regression tests and reproductions
fix the order by holding the manager's own lock while the monitor thread waits
on it, which shows the window exists, not how often it is hit.
* HDDS-17402 needs an Error on the monitor thread, in practice native thread
exhaustion caused elsewhere in the process. It was run outside the test suite
at the per process thread limit; the regression test stands in for it with a
resource whose {{hashCode}} throws.
* The SCM side of each issue was argued from the code, not run on a cluster.
* The patches were built and tested on the pinned commit and apply to master at
a7da4f70195. All three add tests at the end of {{TestLeaseManager}} and touch
its imports, and HDDS-17404 and HDDS-17402 both change the same block of
{{LeaseMonitor.run}}, so the second and third to land need a rebase.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify lease-manager (Apache Ozone master @f804bf2)
> -------------------------------------------------------------
>
> Key: HDDS-16580
> URL: https://issues.apache.org/jira/browse/HDDS-16580
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: lease-manager.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
> {{lease-manager}}. Scope and code entry points are in the attached guidance
> file [^lease-manager.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: f804bf26867246067017fdd9e5319c2cbdbd5db8
> 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 \
> "lease-manager|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]
