[
https://issues.apache.org/jira/browse/HDDS-16431?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Siyao Meng reassigned HDDS-16431:
---------------------------------
Assignee: Siyao Meng
> 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
> 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: [email protected]
For additional commands, e-mail: [email protected]
