Siyao Meng created HDDS-16433:
---------------------------------
Summary: 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
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).
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
