[
https://issues.apache.org/jira/browse/HDDS-16469?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18125924#comment-18125924
]
Siyao Meng commented on HDDS-16469:
-----------------------------------
Follow up: the 13 code review candidates that the first run left unjudged
(CR-2, CR-4, CR-5 and CR-7 to CR-16) have now each been investigated against
the pinned commit. This supersedes the "Not judged" section of the result
comment above.
h3. Run environment
{noformat}
Ozone commit: 20e6a1c0f6039248373efd3eb1d7f2afcf7f1535 (unmodified, no trace
instrumentation)
Specula: v1.2.0 with local changes
Agent/model: claude-code, Claude Opus 5.5 (1M context)
Effort: medium
Scope: bug confirmation and severity classification for these 13
candidates only
Total: about 1h agent time, about $19 (estimate)
{noformat}
The candidate records were recovered unchanged from the first consolidation
pass, so no fresh consolidation was needed.
h3. Result
||Disposition||Count||
|Reproduced|0|
|False positive|11|
|Dropped, already reported|2|
No new issue is filed from these 13. Final count for this subtask: 20
candidates, 5 reproduced (HDDS-16732 to HDDS-16736), 13 false positive, 2
dropped as already reported.
h3. Dispositions
||Candidate||Claim||Disposition||
|CR-2|The open time and commit time checks report the same race with different
result codes|False positive. The split is the S3 contract added on purpose by
HDDS-14968: 412 when the condition is false when evaluated, 409 when a
conflicting write lands during the upload. Existing tests assert both sides.|
|CR-4|{{CreateFile}} ignores {{expectedETag}}|False positive. True on the OM
side, but the client side translator never sends the field on {{CreateFile}},
so it takes a hand built request.|
|CR-5|FSO bulk delete enforces no condition|False positive.
{{OmKeysDeleteRequestWithFSO}} inherits the {{updateIDs}} check of
{{OMKeysDeleteRequest}}. Stale IDs were rejected per key and nothing was
deleted.|
|CR-7|A key listed twice in one {{DeleteKeys}} request releases quota
twice|Dropped, already reported as HDDS-16773.|
|CR-8|A zero length commit does not enqueue its preallocated blocks|False
positive. Deliberate since HDDS-14417. A mini cluster run found no datanode
trace of those blocks and no bucket usage.|
|CR-9|{{filterOutBlocksStillInUse}} can throw {{IllegalStateException}} on a
repeated block|False positive. No sequence was found that puts a repeated block
into the key (create, allocate and commit were run, hsync and lease recovery
were read). The exception fired only on a hand built open key.|
|CR-10|FSO commit rebuilds the key info before {{validateAtomicRewrite}}, the
reverse of the non FSO order|False positive. The work before the check is on a
request private copy. After a rejected commit the open key, the winner's key,
bucket usage and {{deletedTable}} were unchanged, same as non FSO.|
|CR-11|MPU complete reads the key table inline, not through the FSO
accessor|False positive. The inline read already uses the FSO key and the file
table. Six conditional cases on an FSO bucket returned the correct result.|
|CR-12|{{createKeyIfNotExists}} gates on {{ATOMIC_REWRITE_KEY}}, not
{{ATOMIC_CREATE_IF_NOT_EXISTS}}|Dropped, already reported in HDDS-16734
(suggested fix, item 3).|
|CR-13|A metadata only write fails an in flight conditional commit|False
positive. Documented design ({{overwrite-key-only-if-unchanged.md}}). The
conflict is retryable, and it keeps a concurrent ACL change from being lost.|
|CR-14|The old sentinel name {{EXPECTED_GEN_CREATE_IF_NOT_EXISTS}} is left
behind|False positive as a bug. Comments, Javadoc and one design doc line only.|
|CR-15|Removed {{KeyInfo}} field 23 is not reserved|False positive as a bug.
The field was added and removed within the 2.2.0 cycle, no release wrote it and
nothing reads it.|
|CR-16|The {{setExpectedDataGeneration(null)}} scrub in both commit paths is
redundant|False positive. The scrub is still what clears the field on the key
table cache entry. Only the comments differ.|
h3. Possible cleanups seen on the way
None of these is a bug at this commit, so none is filed.
* {{OMFileCreateRequest.preExecute}} could reject a request that carries
{{expectedETag}} or {{expectedDataGeneration}} (CR-4).
* The {{Collectors.toMap}} in {{filterOutBlocksStillInUse}} could take a merge
function, so a future change to block grouping cannot turn into an OM shutdown
(CR-9).
* {{KeyInfo}} could declare {{reserved 23}} (CR-15).
* {{testUpdateIDCountMatchKeyCount}} in {{TestOMKeysDeleteRequest}} and
{{TestOMKeysDeleteRequestWithFSO}} builds an empty {{updateIDs}} list, so it
never exercises the check (CR-5).
* {{s3-conditional-requests.md}} still says a commit time mismatch returns
{{KEY_NOT_FOUND}}. Since HDDS-14968 it returns {{ATOMIC_WRITE_CONFLICT}} (CR-2).
h3. Caveats
* All 13 ended with the investigator dismissing the candidate, and the
Challenger debate opens only for a candidate the investigator upholds, so none
of the 13 went through a debate round.
* The two dropped candidates were not reproduced again here. Their
reproductions are on the issues that already track them.
* CR-2 and CR-10 needed a second attempt because the first ended before its
build finished.
Generated with Specula (Claude Opus 5.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]
