Siyao Meng created HDDS-16429:
---------------------------------
Summary: Formal verification for Ozone OM key lifecycle and FSO
deletion with TLA+
Key: HDDS-16429
URL: https://issues.apache.org/jira/browse/HDDS-16429
Project: Apache Ozone
Issue Type: Sub-task
Reporter: Siyao Meng
Use TLA+ (via the Specula pipeline) to model and verify the OM key lifecycle
and FSO deletion paths: lifecycle rule scan and move to trash, per key updateID
guards across delete and rename, FSO recursive directory deletion with batch
split, and crash and resume of the deleting services. Model check the
specification and validate real OM traces against it. Bugs found by this effort
are linked under this issue.
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-key-lifecycle|high|{{campaigns/ozone-9fbf9ee/targets/006-om-key-lifecycle/.prompt-extra.md}}|1
reproduced Critical, 2 masked High|
|om-fso-recursive-deletion|high|{{campaigns/ozone-9fbf9ee/targets/005-om-fso-recursive-deletion/.prompt-extra.md}}|1
reproduced Medium, 1 masked Medium|
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
\
"<target>|apache/ozone|Java|Use the target-specific .prompt-extra.md"
{code}
h3. Bugs (link via "Testing discovered")
* (REPRODUCED, Critical) BUG_KEYLC_CR4: the LEGACY (non FSO) rename handler
lacks the per key updateID guard that the delete and FSO rename paths enforce,
so a lifecycle move to trash carrying a scan captured stale updateID
destructively moves a live, overwritten key into trash where reads return not
found and retention later purges it. Durable, no automatic recovery, reachable
in the default configuration. [om-key-lifecycle CR-4]
* (REPRODUCED, Medium) BUG_FSO_CR7: the directory deleting service can purge a
parent directory before its descendants are durably safe under batch split
combined with a crash. [om-fso-recursive-deletion CR-7]
* (MASKED, High) BUG_KEYLC_MC1: cache first unordered enumeration breaks the
descending order premise of canSkipDir, so on crash or resume an unscanned FSO
directory is skipped and its expired keys are not collected. [om-key-lifecycle
MC-1]
* (MASKED, High) BUG_KEYLC_MC2: a parent directory emptied during a scan is
queued for expiry only in memory, so a crash after the cursor advances past it
but before its deletion flushes strands the emptied directory.
[om-key-lifecycle MC-2]
* (MASKED, Medium) BUG_FSO_CR5: a real NPE in submitPurgePathsWithBatching is
swallowed by the BackgroundService catch(Throwable) and periodic retry, no
durable harm today. [om-fso-recursive-deletion CR-5]
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]
