[
https://issues.apache.org/jira/browse/HDDS-16430?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Siyao Meng updated HDDS-16430:
------------------------------
Description:
Use TLA+ (via the Specula pipeline) to model and verify the OM
SnapshotDiffManager job lifecycle: submit, cancel, resubmit, generation
transitions, the persisted job report, and the diff cleanup service, across OM
upgrade and crash. Model check the specification and validate real OM traces
against it. Bugs found by this effort are linked under this issue. Related to
the snapshot lifecycle effort in HDDS-15927.
h3. Run environment
{noformat}
Ozone commit: 9fbf9ee0cb1bd2f5f5d437b6719ebbe5309351fb
Specula: v1.1.0 (commit c6aa3dfa)
Agent/model: claude-code, Claude Opus 4.8 (1M context)
{noformat}
h3. Coverage
||Target||Effort||Guidance||Result||
|om-snapshot-diff-jobs|high|{{campaigns/ozone-9fbf9ee/targets/009-om-snapshot-diff-jobs/.prompt-extra.md}}|4
reproduced (2 Critical, 1 High, 1 Low)|
h3. Reproduce
{code:none}
specula run --agent=claude-code --effort=high --keep-original --max-parallel=2 \
--enable-reviews --confirm-debate --tlc-memory-limit=28G --tlc-worker-limit=8
\
"om-snapshot-diff-jobs|apache/ozone|Java|Use the target-specific
.prompt-extra.md"
{code}
h3. Bugs (link via "Testing discovered")
* (REPRODUCED, Critical) HDDS-16441: a cancelled generation's task publishes
its result as the new generation's DONE, so the submit, cancel, resubmit path
leaves a report the reader trusts wrongly. [MC-1]
* (REPRODUCED, Critical) HDDS-16442: after a routine OM upgrade every pre
existing DONE snapshot diff job deserializes with a null largestEntryKey, so
the first client read of the report trips the integrity check and hits an
uncaught failure. [CR-2]
* (REPRODUCED, High) HDDS-16443: on resubmit of a terminal job the cleanup
service can purge the freshly created live generation between the two persisted
writes, deleting the active row and crashing the client resubmit RPC. [MC-2]
* (REPRODUCED, Low) HDDS-16444: a terminal job resubmit raises an
IllegalStateException that masks the original cause. [CR-3]
Generated with Specula (Claude Opus 4.8).
was:
Use TLA+ (via the Specula pipeline) to model and verify the OM
SnapshotDiffManager job lifecycle: submit, cancel, resubmit, generation
transitions, the persisted job report, and the diff cleanup service, across OM
upgrade and crash. Model check the specification and validate real OM traces
against it. Bugs found by this effort are linked under this issue. Related to
the snapshot lifecycle effort in HDDS-15927.
h3. Run environment
{noformat}
Ozone commit: 9fbf9ee0cb1bd2f5f5d437b6719ebbe5309351fb
Specula: v1.1.0 (commit c6aa3dfa)
Agent/model: claude-code, Claude Opus 4.8 (1M context)
{noformat}
h3. Coverage
||Target||Effort||Guidance||Result||
|om-snapshot-diff-jobs|high|{{campaigns/ozone-9fbf9ee/targets/009-om-snapshot-diff-jobs/.prompt-extra.md}}|4
reproduced (2 Critical, 1 High, 1 Low)|
h3. Reproduce
{code:none}
specula run --agent=claude-code --effort=high --keep-original --max-parallel=2 \
--enable-reviews --confirm-debate --tlc-memory-limit=28G --tlc-worker-limit=8
\
"om-snapshot-diff-jobs|apache/ozone|Java|Use the target-specific
.prompt-extra.md"
{code}
h3. Bugs (link via "Testing discovered")
* (REPRODUCED, Critical) BUG_SDIFF_MC1: a cancelled generation's task publishes
its result as the new generation's DONE, so the submit, cancel, resubmit path
leaves a report the reader trusts wrongly. [MC-1]
* (REPRODUCED, Critical) BUG_SDIFF_CR2: after a routine OM upgrade every pre
existing DONE snapshot diff job deserializes with a null largestEntryKey, so
the first client read of the report trips the integrity check and hits an
uncaught failure. [CR-2]
* (REPRODUCED, High) BUG_SDIFF_MC2: on resubmit of a terminal job the cleanup
service can purge the freshly created live generation between the two persisted
writes, deleting the active row and crashing the client resubmit RPC. [MC-2]
* (REPRODUCED, Low) BUG_SDIFF_CR3: a terminal job resubmit raises an
IllegalStateException that masks the original cause. [CR-3]
Generated with Specula (Claude Opus 4.8).
> Formal verification for Ozone OM snapshot diff jobs with TLA+
> -------------------------------------------------------------
>
> Key: HDDS-16430
> URL: https://issues.apache.org/jira/browse/HDDS-16430
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Priority: Major
>
> Use TLA+ (via the Specula pipeline) to model and verify the OM
> SnapshotDiffManager job lifecycle: submit, cancel, resubmit, generation
> transitions, the persisted job report, and the diff cleanup service, across
> OM upgrade and crash. Model check the specification and validate real OM
> traces against it. Bugs found by this effort are linked under this issue.
> Related to the snapshot lifecycle effort in HDDS-15927.
> h3. Run environment
> {noformat}
> Ozone commit: 9fbf9ee0cb1bd2f5f5d437b6719ebbe5309351fb
> Specula: v1.1.0 (commit c6aa3dfa)
> Agent/model: claude-code, Claude Opus 4.8 (1M context)
> {noformat}
> h3. Coverage
> ||Target||Effort||Guidance||Result||
> |om-snapshot-diff-jobs|high|{{campaigns/ozone-9fbf9ee/targets/009-om-snapshot-diff-jobs/.prompt-extra.md}}|4
> reproduced (2 Critical, 1 High, 1 Low)|
> h3. Reproduce
> {code:none}
> specula run --agent=claude-code --effort=high --keep-original
> --max-parallel=2 \
> --enable-reviews --confirm-debate --tlc-memory-limit=28G
> --tlc-worker-limit=8 \
> "om-snapshot-diff-jobs|apache/ozone|Java|Use the target-specific
> .prompt-extra.md"
> {code}
> h3. Bugs (link via "Testing discovered")
> * (REPRODUCED, Critical) HDDS-16441: a cancelled generation's task publishes
> its result as the new generation's DONE, so the submit, cancel, resubmit path
> leaves a report the reader trusts wrongly. [MC-1]
> * (REPRODUCED, Critical) HDDS-16442: after a routine OM upgrade every pre
> existing DONE snapshot diff job deserializes with a null largestEntryKey, so
> the first client read of the report trips the integrity check and hits an
> uncaught failure. [CR-2]
> * (REPRODUCED, High) HDDS-16443: on resubmit of a terminal job the cleanup
> service can purge the freshly created live generation between the two
> persisted writes, deleting the active row and crashing the client resubmit
> RPC. [MC-2]
> * (REPRODUCED, Low) HDDS-16444: a terminal job resubmit raises an
> IllegalStateException that masks the original cause. [CR-3]
> Generated with Specula (Claude Opus 4.8).
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
