[
https://issues.apache.org/jira/browse/HDDS-16573?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18129892#comment-18129892
]
Siyao Meng commented on HDDS-16573:
-----------------------------------
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
Challenger debate, and severity classification.
h3. Run environment
{noformat}
Ozone commit: b10a7d427bdf83807a7e48a1be507d3b02d5a503
Specula: v1.2.0-34-gcdd19e39, with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
TLC limits: 40G memory, 20 workers
Total: 6h 5m agent time, 103.1M tokens, about $65 (estimate)
{noformat}
h3. Result
13 candidate findings came out of model checking (5) and code review (8), and
all 13 were investigated individually.
||Disposition||Count||
|Reproduced|4|
|Limited by the test environment (argued from code)|1|
|Masked (defect present, harm currently covered elsewhere)|1|
|False positive|6|
|Dropped as already reported|1|
Each filed finding 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, the bug was confirmed still present on apache
master (checked on 2026-10-21), and the fix patch and report were reviewed
independently before filing.
h3. Filed
||Issue||Priority||Summary||
|HDDS-17272|Major|Interrupted S3 PUT to an encrypted bucket fails but commits
an empty object with the full body's ETag, replacing the previous version|
|HDDS-17273|Minor|S3 PUT or UploadPart that fails with an Error after the body
is copied still commits, skipping the Content-MD5 and x-amz-content-sha256
checks|
|HDDS-17271|Minor|KeyOutputStream releases a request permit it never acquired
when write, flush or hsync is interrupted|
|HDDS-17290|Major|Close on an interrupted thread fails but OM still commits the
key, so a small encrypted file or an interrupted write becomes empty or
truncated|
Priorities follow the manual validation, not the pipeline's severity classes.
Each issue has a proposed fix patch with regression tests and a standalone
reproduction test. HDDS-17290 was found while validating HDDS-17272: the same
commit on an interrupted close also happens outside the S3 gateway.
h3. Not filed or closed
* Three reproduced findings, and one more found during validation, need the
legacy bucket versioning flag, which turns on the multi version key path that
HDDS-16127 treats as unused and HDDS-15728 will replace:
** HDDS-17287 (a commit keeps older versions whose blocks are no longer
referenced) and HDDS-17282 (a snapshot reclaim check that misses earlier
version groups, found during validation) were filed and then resolved Not A
Problem for that reason.
** The multipart upload complete path replaces the latest version in place
without queueing the blocks it replaced: not filed for the same reason.
** Open key expiry can send the live key's inherited blocks for deletion:
duplicates HDDS-16732.
* Dropped as already reported: one finding duplicates HDDS-16661
(apache/ozone#11586).
* False positives: six code review findings, including the claim that two
conditional PUTs can both win, which no explored interleaving produced.
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=40G --tlc-worker-limit=20 \
"s3-put-commit-guard|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* HDDS-17273 needs a java.lang.Error after the body is copied, realistically an
OutOfMemoryError; it was shown with an injected Error, not with real memory
pressure.
* The patches were built and tested on the pinned commit and apply to master at
1ff29ee6b86.
* HDDS-17272 and HDDS-17273 change S3ObjectWriteGuard, which open
apache/ozone#11586, #11589 and #11562 also change; whichever lands second will
need a rebase.
* The patches are proposals for review.
Generated with Specula (Claude Opus 5.5).
> [Specula] Verify s3-put-commit-guard (Apache Ozone master @b10a7d4)
> -------------------------------------------------------------------
>
> Key: HDDS-16573
> URL: https://issues.apache.org/jira/browse/HDDS-16573
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: specula
> Attachments: s3-put-commit-guard.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
> {{s3-put-commit-guard}}. Scope and code entry points are in the attached
> guidance file [^s3-put-commit-guard.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: b10a7d427bdf83807a7e48a1be507d3b02d5a503
> 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 \
> "s3-put-commit-guard|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]
