[
https://issues.apache.org/jira/browse/HDDS-16429?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Siyao Meng updated HDDS-16429:
------------------------------
Description:
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) HDDS-16436: 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) HDDS-16437: 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) HDDS-16438: 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) HDDS-16439: 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) HDDS-16440: 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).
was:
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).
> 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
> Priority: Major
>
> 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) HDDS-16436: 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) HDDS-16437: 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) HDDS-16438: 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) HDDS-16439: 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) HDDS-16440: 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]
