Siyao Meng created HDDS-16431:
---------------------------------
Summary: Formal verification for Ozone SCM ReplicationManager and
container replication with TLA+
Key: HDDS-16431
URL: https://issues.apache.org/jira/browse/HDDS-16431
Project: Apache Ozone
Issue Type: Sub-task
Reporter: Siyao Meng
Use TLA+ (via the Specula pipeline) to model and verify the SCM
ReplicationManager: over and under replication handling, RATIS and EC replica
counting, BCSID and origin selection, quasi closed recovery, pending replica
operations and their accounting, container lifecycle state, and leadership
transfer. Model check the specification and validate real SCM 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||
|scm-ratis-replication|medium|{{campaigns/ozone-9fbf9ee/targets/012-scm-ratis-replication/.prompt-extra.md}}|2
reproduced High, 1 masked High|
|scm-pending-replica-ops|medium|{{campaigns/ozone-9fbf9ee/targets/014-scm-pending-replica-ops/.prompt-extra.md}}|1
reproduced High, 1 reproduced Low|
|scm-container-lifecycle|medium|{{campaigns/ozone-9fbf9ee/targets/015-scm-container-lifecycle/.prompt-extra.md}}|1
reproduced High, 1 masked Medium|
|scm-ec-replication|medium|{{campaigns/ozone-9fbf9ee/targets/013-scm-ec-replication/.prompt-extra.md}}|No
findings|
h3. Reproduce
{code:none}
specula run --agent=claude-code --effort=medium --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_SCMRATIS_MC1: a split lock read in
processOverReplicatedContainer issues an extra delete against a live replica,
dropping a CLOSED RF=3 container below its replication factor.
[scm-ratis-replication MC-1]
* (REPRODUCED, High) BUG_SCMRATIS_CR2: for quasi closed stuck containers an
UNHEALTHY IN_SERVICE replica is counted as valid, so an origin with only one
healthy copy is declared adequately replicated and a later over delete can
remove the healthy copy. [scm-ratis-replication CR-2]
* (REPRODUCED, High) BUG_PENDING_MC2: an out of lock race re inserts a DELETE
op for an already deleted replica, producing an orphaned, never confirmable op
that is resent every RM cycle and inflates the inflight delete accounting.
[scm-pending-replica-ops MC-2]
* (REPRODUCED, High) BUG_CLC_MC3: a CLOSED container's immutable sequenceId is
silently bumped by a healthy higher BCSID replica report, so quorum correct
QUASI_CLOSED replicas are reclassified as unhealthy and a fully replicated
container is treated as under replicated and its replicas are stranded.
[scm-container-lifecycle MC-3]
* (MASKED, High) BUG_SCMRATIS_MC2: on SCM leadership transfer the new leader
clears pending ops and schedules a redundant delete on a different replica,
dropping below RF if both deletes land, currently masked by datanode term gate
timing. [scm-ratis-replication MC-2]
* (REPRODUCED, Low) BUG_PENDING_CR3: repeated per replica expiry re counts one
replica as many timed out replicas, contradicting the documented
ReplicationManagerMetrics meaning. [scm-pending-replica-ops CR-3]
* (MASKED, Medium) BUG_CLC_CR4: a cross lock lost update of a shared
ContainerInfo sequenceId, masked by periodic report resend and writeLock
serialized durable state. [scm-container-lifecycle CR-4]
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]
