Siyao Meng created HDDS-16430:
---------------------------------
Summary: 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
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).
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
