[jira] [Assigned] (HDDS-16429) Formal verification for Ozone OM key lifecycle and FSO deletion with TLA+

["Siyao Meng (Jira)" <ji...@apache.org>]

     [ https://issues.apache.org/jira/browse/HDDS-16429?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel ]

Siyao Meng reassigned HDDS-16429:
---------------------------------

    Assignee: Siyao Meng

> 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
>            Assignee: 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: issues-unsubscribe@ozone.apache.org
For additional commands, e-mail: issues-help@ozone.apache.org