[
https://issues.apache.org/jira/browse/HDDS-16431?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Siyao Meng updated HDDS-16431:
------------------------------
Description:
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) HDDS-16445: 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) HDDS-16446: 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) HDDS-16447: 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) HDDS-16448: 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) HDDS-16449: 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) HDDS-16450: 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) HDDS-16451: 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).
was:
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).
> 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
> Priority: Major
>
> 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) HDDS-16445: 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) HDDS-16446: 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) HDDS-16447: 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) HDDS-16448: 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) HDDS-16449: 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) HDDS-16450: 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) HDDS-16451: 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]
