[
https://issues.apache.org/jira/browse/HDDS-16433?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Siyao Meng reassigned HDDS-16433:
---------------------------------
Assignee: Siyao Meng
> Formal verification for Ozone DataNode container replication, EC
> reconstruction, and disk balancer with TLA+
> ------------------------------------------------------------------------------------------------------------
>
> Key: HDDS-16433
> URL: https://issues.apache.org/jira/browse/HDDS-16433
> 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 DataNode side
> container replication: EC reconstruction and scrub interaction, the container
> state machine, block deletion, and DiskBalancer container moves, across crash
> and restart reconciliation. Model check the specification and validate real
> DataNode 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||
> |dn-ec-reconstruction|high|{{campaigns/ozone-9fbf9ee/targets/022-dn-ec-reconstruction/.prompt-extra.md}}|2
> reproduced High, 1 masked Low|
> |dn-disk-balancer|medium|{{campaigns/ozone-9fbf9ee/targets/021-dn-disk-balancer/.prompt-extra.md}}|2
> reproduced High, 1 masked Medium|
> |dn-block-deletion|medium|{{campaigns/ozone-9fbf9ee/targets/017-dn-block-deletion/.prompt-extra.md}}|1
> masked Medium|
> |dn-container-state-machine|medium|{{campaigns/ozone-9fbf9ee/targets/020-dn-container-state-machine/.prompt-extra.md}}|1
> env-limited High|
> h3. Reproduce
> {code:none}
> specula run --agent=claude-code --effort=<effort> --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, High) HDDS-16455: a stale scrub task silently demotes a
> successfully CLOSED reconstructed EC replica to UNHEALTHY with no ICR, so on
> the next full container report SCM deletes and re reconstructs a valid
> replica. [dn-ec-reconstruction MC-1]
> * (REPRODUCED, High) HDDS-16456: a non atomic timeout re arm on the write RPC
> tail resurrects a recoveringContainerMap entry for a container that
> concurrently moved to CLOSING or CLOSED, and the scrub then marks that valid
> replica UNHEALTHY. [dn-ec-reconstruction MC-2]
> * (REPRODUCED, High) HDDS-16457: an EC replica move plus a mid move crash and
> restart leaves a durable two copy inconsistency (CLOSED source plus UNHEALTHY
> destination) that no DataNode local mechanism reclaims. [dn-disk-balancer
> MC-1]
> * (REPRODUCED, High) HDDS-16458: after a DiskBalancer EC move a crash before
> the source is durably marked for delete drops the volatile pending deletion
> queue, and restart reconciliation leaves the extra copy. [dn-disk-balancer
> MC-2]
> * (ENV_LIMITED, High) HDDS-16459: a non atomic snapshot of (lastAppliedIndex,
> container2BCSIDMap) can mark a healthy container UNHEALTHY after a crash that
> loses the unsynced container WAL while the Ratis snapshot survives, driving
> unnecessary re replication, env-limited to crash with selective WAL loss.
> [dn-container-state-machine CR-2]
> * (MASKED, Low) HDDS-16460: the container delete path leaves a zombie
> recoveringContainerMap entry, masked at HEAD by the scrub null guard, non
> reused container IDs, and auto create rejection, a hygiene gap.
> [dn-ec-reconstruction MC-3]
> * (MASKED, Medium) HDDS-16461: an asymmetric decrement leaves the persisted
> pendingDeleteBlockCount inflated on a drained container, masked by
> resetPendingDeleteBlockCount on restart, surfacing only as one wasted
> deletion pass. [dn-block-deletion MC-1]
> 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]
