You are viewing a plain text version of this content. The canonical link for it is here.
Posted to issues@ozone.apache.org by "Siyao Meng (Jira)" <ji...@apache.org> on 2026/09/15 23:58:00 UTC
[jira] [Updated] (HDDS-16433) Formal verification for Ozone DataNode container replication, EC reconstruction, and disk balancer with TLA+
[ https://issues.apache.org/jira/browse/HDDS-16433?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel ]
Siyao Meng updated HDDS-16433:
------------------------------
Description:
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: real defect reachable only outside the modeled configuration; classify by consequence. [dn-container-state-machine CR-2]
* (MASKED, Low) HDDS-16460: masked; classify by consequence with the mask named. [dn-ec-reconstruction MC-3]
* (MASKED, Medium) HDDS-16461: masked; classify by consequence with the mask named. [dn-block-deletion MC-1]
Generated with Specula (Claude Opus 4.8).
was:
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) BUG_ECRECON_MC1: 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) BUG_ECRECON_MC2: 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) BUG_DISKBAL_MC1: 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) BUG_DISKBAL_MC2: 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) BUG_DNCSM_CR2: real defect reachable only outside the modeled configuration; classify by consequence. [dn-container-state-machine CR-2]
* (MASKED, Low) BUG_ECRECON_MC3: masked; classify by consequence with the mask named. [dn-ec-reconstruction MC-3]
* (MASKED, Medium) BUG_BLKDEL_MC1: masked; classify by consequence with the mask named. [dn-block-deletion MC-1]
Generated with Specula (Claude Opus 4.8).
> 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
> 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: real defect reachable only outside the modeled configuration; classify by consequence. [dn-container-state-machine CR-2]
> * (MASKED, Low) HDDS-16460: masked; classify by consequence with the mask named. [dn-ec-reconstruction MC-3]
> * (MASKED, Medium) HDDS-16461: masked; classify by consequence with the mask named. [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: issues-unsubscribe@ozone.apache.org
For additional commands, e-mail: issues-help@ozone.apache.org