[
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: [email protected]
For additional commands, e-mail: [email protected]
