[
https://issues.apache.org/jira/browse/HDDS-16469?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18123635#comment-18123635
]
Siyao Meng commented on HDDS-16469:
-----------------------------------
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: 20e6a1c0f6039248373efd3eb1d7f2afcf7f1535
Specula: v1.2.0
Agent/model: claude-code, Claude Opus 5 (1M context)
Effort: medium
TLC limits: 28G memory, 8 workers
Phases 1 to 3: 5h 58m, 113.5M tokens, about $98, plus four partial Phase 4a
passes
{noformat}
h3. Result
20 candidate findings were consolidated from model checking (MC-1 to MC-7) and
code review (CR-2 to CR-16), then investigated individually.
||Disposition||Count||
|Reproduced|5|
|False positive|2|
|Incomplete (not judged, see caveats)|13|
Severity of the 5 reproduced findings: 4 Critical, 1 High. Every one reached
consensus in the debate round, with the Challenger agreeing with the
investigator rather than being overruled.
h3. Reproduced bugs proposed for filing
* (Critical) On a versioned bucket, an abandoned open key created over a live
key inherits the live key's block version groups, and the open key reaper puts
every group into {{deletedTable}} with no reference check, so a committed key's
blocks are handed to the SCM delete path. {{filterOutBlocksStillInUse}},
written for exactly this hazard, is wired into the three commit paths but not
the reaper. Reproduced at escalation level 0, no fault injection. [MC-1]
* (Critical) Two writers opening the same not-yet-existing key on a versioned
bucket: neither open key inherits anything, and the second commit skips the
overwrite-cleanup branch because versioning is on, so the first committed
version is silently discarded and its blocks are referenced by nothing and
queued for deletion by nothing. Permanently leaked, and the bucket namespace
counter is inflated. [MC-2]
* (Critical) Conditional delete and conditional MPU complete send their
condition to the server with no capability gate on either side. {{RpcClient}}
guards every other conditional entry point on {{ATOMIC_REWRITE_KEY}} but not
{{deleteKey(..., expectedETag)}} or {{completeMultipartUpload(...)}}, and
server side neither {{OMKeyDeleteRequest}} nor
{{S3MultipartUploadCompleteRequest}} calls {{checkFeatureEnabled}}. An OM that
does not implement the condition ignores the unknown optional field and answers
success, so a compare and delete destroys a newer value while the caller is
told the condition held. [MC-3]
* (Critical) A writer that opens a key with a condition and then calls hsync
makes its own condition permanently unsatisfiable: the hsync write back keeps
the condition on the open key record, hsync itself publishes the key, and the
commit time recheck has no same writer exemption. {{isSameHsyncKey}} is
computed but consumed only for quota accounting. The client is told its write
failed while its partial data stays live, and both OM repair paths fail the
same check forever. [MC-5]
* (High) {{CommitKey}} is non idempotent by construction, and the Ratis retry
cache that hides it is unavailable on the S3 path because
{{OzoneManagerServiceGrpc}} mints a random {{ClientId}} per request. An
ordinary timeout retry makes the write durable while the client receives
{{KEY_NOT_FOUND}}. [MC-4]
h3. Fix patches
Four of the five carry a fix patch, attached to their own issue, each against
the pinned commit with a regression test added to the existing suite rather
than a new one, verified to fail without the change and pass with it, and
checkstyle clean.
||Finding||Patch||
|MC-1|{{MC-1-open-key-reaper-retains-live-blocks.patch}}|
|MC-2|{{MC-2-versioned-overwrite-orphans-previous-blocks.patch}}, reclaims the
orphaned blocks and fixes the namespace count; true version retention is left
to reviewers|
|MC-3|{{MC-3-gate-conditional-delete-and-mpu-complete.patch}}, also closes the
ETag only gap the existing create and commit gates had|
|MC-5|{{MC-5-conditional-commit-survives-own-hsync.patch}}|
|MC-4|none, filed as analysis only because the fix needs a persisted writer
identity or a new protocol field, both reviewer decisions|
h3. False positives
MC-6 (If-Match: * against an existing key carrying no ETag) and MC-7 were
investigated and dismissed.
h3. Not judged
The 13 code review candidates CR-2, CR-4, CR-5 and CR-7 to CR-16 were never
confirmed. The confirmation batch was cut by an infrastructure budget limit on
the model gateway after the first five findings, and a later interaction
between the spec repair loop and the ordinary confirmation pass rewrote the
candidate catalogue down to the model checking violations, so their candidate
records no longer exist in the run directory. Their descriptions survive in
{{confirmed-bugs.md}}. They carry no verdict and no impact claim, and nothing
should be concluded about them either way. Re-running confirmation for this
target would need a fresh consolidation pass.
h3. Reproduce
{code:none}
specula run --agent=claude-code --effort=medium --model='claude-opus-5[1m]' \
--max-parallel=2 --enable-reviews --confirm-debate \
--tlc-memory-limit=28G --tlc-worker-limit=8 \
"om-conditional-key|apache/ozone|Java|Use the target-specific guidance"
{code}
h3. Caveats
* Phase 4a needed four passes. Pass 1 aborted for all 20 findings because the
per finding {{git worktree add}} could not complete inside the workspace on
this host. Pass 2 reached real verdicts but was cut after five findings by the
gateway budget limit. Pass 3 was the spec repair loop (requests RR-001 and
RR-002), which confirmed MC-1 to MC-5 with debate consensus. Pass 4 was an
ordinary pass that produced no further verdicts and reduced the candidate
catalogue, so the report was restored to the pass 3 state before severity
classification ran. The 5 reproduced verdicts and their evidence come from pass
3 and are unaffected.
* MC-2's trigger needs bucket versioning enabled, which is reachable through
the native Java client but not through the CLI or the S3 gateway.
* MC-4's externally visible harm needs the gRPC OM transport; the default
Hadoop RPC retry cache masks it.
* MC-5's trigger needs {{ozone.fs.hsync.enabled}} and
{{ozone.client.hbase.enhancements.allowed}}, both of which default to false.
* MC-1's reproduction stops where OM hands the live block to the SCM delete
path. The final DataNode level block removal was not executed, since a request
level unit test has no SCM or DataNode.
* Novelty was checked against both the repository's merged git history and open
HDDS issues. The nearest neighbours found were HDDS-15167 (MPU complete
conflict detection, a different concern) and the active S3 object versioning
work under HDDS-15728, which overlaps MC-2's retention half but not its block
leak.
* Model checking and trace validation ran against 6 collected trace scenarios
covering hsync self conflict, lost reply and retry, open key block inheritance,
conditional delete drop, the ETag sentinel zero case, and delete ETag rejection.
Generated with Specula (Claude Opus 5).
> [Specula] Verify om-conditional-key (Apache Ozone master @20e6a1c)
> ------------------------------------------------------------------
>
> Key: HDDS-16469
> URL: https://issues.apache.org/jira/browse/HDDS-16469
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Assignee: Siyao Meng
> Priority: Minor
> Labels: help-wanted, specula
> Attachments: om-conditional-key.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
> {{om-conditional-key}}. Scope and code entry points are in the attached
> guidance file [^om-conditional-key.guidance.md].
> h3. Run environment
> {noformat}
> Apache Ozone commit: 20e6a1c0f6039248373efd3eb1d7f2afcf7f1535
> 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 \
> "om-conditional-key|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
> * 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]
