[jira] [Commented] (HDDS-16431) [Specula] Verify scm-ratis-replication, scm-pending-replica-ops, scm-container-lifecycle and scm-ec-replication (Apache Ozone master @9fbf9ee)

["Siyao Meng (Jira)" <ji...@apache.org>]

    [ https://issues.apache.org/jira/browse/HDDS-16431?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18125914#comment-18125914 ] 

Siyao Meng commented on HDDS-16431:
-----------------------------------

Verification run complete. All four targets ran through the full Specula pipeline at Ozone 9fbf9ee0cb1bd2f5f5d437b6719ebbe5309351fb (Specula v1.1.0, claude-code, Claude Opus 4.8).

||Target||Effort||Result||
|scm-ratis-replication|medium|HDDS-16445 (reproduced, High), HDDS-16446 (reproduced, High), HDDS-16449 (masked, High)|
|scm-pending-replica-ops|medium|HDDS-16447 (reproduced, High), HDDS-16450 (reproduced, Low)|
|scm-container-lifecycle|medium|HDDS-16448 (reproduced, High), HDDS-16451 (masked, Medium)|
|scm-ec-replication|medium|No findings|

All seven bugs are linked to this issue with the Testing link type. The run environment, coverage and per bug summaries are in the description. Resolving as Done.

> [Specula] Verify scm-ratis-replication, scm-pending-replica-ops, scm-container-lifecycle and scm-ec-replication (Apache Ozone master @9fbf9ee)
> ----------------------------------------------------------------------------------------------------------------------------------------------
>
>                 Key: HDDS-16431
>                 URL: https://issues.apache.org/jira/browse/HDDS-16431
>             Project: Apache Ozone
>          Issue Type: Sub-task
>            Reporter: Siyao Meng
>            Assignee: 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: issues-unsubscribe@ozone.apache.org
For additional commands, e-mail: issues-help@ozone.apache.org