[
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: 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).
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) 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).
> 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: 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]
