[
https://issues.apache.org/jira/browse/HDDS-16432?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Siyao Meng updated HDDS-16432:
------------------------------
Description:
Use TLA+ (via the Specula pipeline) to model and verify SCM HA follower catch
up: the inter SCM checkpoint download and install during an apply window, the
SCM HA transaction buffer flush versus durable index, and follower catch up
after leader transfer. Model check the specification and validate real SCM
traces against it. Bugs found by this effort are linked under this issue.
Adjacent to HDDS-16141 (SCM delete-block) and HDDS-16079 (bootstrap checkpoint
install).
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-ha-tx-buffer|medium|{{campaigns/ozone-9fbf9ee/targets/018-scm-ha-tx-buffer/.prompt-extra.md}}|1
reproduced Critical, 1 masked Medium|
|scm-follower-catchup|high|{{campaigns/ozone-9fbf9ee/targets/019-scm-follower-catchup/.prompt-extra.md}}|1
masked Medium|
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, Critical) HDDS-16452: an InterSCMGrpcService.download checkpoint
served during an apply window ships data at index i under the stale durable
index i minus 1, so a follower installs it and durably holds data ahead of its
recorded index. [scm-ha-tx-buffer MC-2]
* (MASKED, Medium) HDDS-16453: an unguarded transaction buffer flush commits
data under a stale index (DurableIndexMatchesData violated), masked by SCM
idempotent replay, with divergence risk the moment a non idempotent replicated
transaction is added. [scm-ha-tx-buffer MC-1]
* (MASKED, Medium) HDDS-16454: a new SCM leader whose apply lags commit drops
reports for committed but unapplied containers as CONTAINER_NOT_FOUND, leaving
replica location accounting incomplete, masked by the WARN only default and
replication manager readiness gating. [scm-follower-catchup MC-2]
Generated with Specula (Claude Opus 4.8).
was:
Use TLA+ (via the Specula pipeline) to model and verify SCM HA follower catch
up: the inter SCM checkpoint download and install during an apply window, the
SCM HA transaction buffer flush versus durable index, and follower catch up
after leader transfer. Model check the specification and validate real SCM
traces against it. Bugs found by this effort are linked under this issue.
Adjacent to HDDS-16141 (SCM delete-block) and HDDS-16079 (bootstrap checkpoint
install).
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-ha-tx-buffer|medium|{{campaigns/ozone-9fbf9ee/targets/018-scm-ha-tx-buffer/.prompt-extra.md}}|1
reproduced Critical, 1 masked Medium|
|scm-follower-catchup|high|{{campaigns/ozone-9fbf9ee/targets/019-scm-follower-catchup/.prompt-extra.md}}|1
masked Medium|
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, Critical) HDDS-16452: an InterSCMGrpcService.download checkpoint
served during an apply window ships data at index i under the stale durable
index i minus 1, so a follower installs it and durably holds data ahead of its
recorded index. [scm-ha-tx-buffer MC-2]
* (MASKED, Medium) HDDS-16453: real defect currently masked; classify by
consequence with the mask named. [scm-ha-tx-buffer MC-1]
* (MASKED, Medium) HDDS-16454: real defect currently masked; classify by
consequence with the mask named. [scm-follower-catchup MC-2]
Generated with Specula (Claude Opus 4.8).
> Formal verification for Ozone SCM HA Ratis follower catch-up and checkpoint
> install with TLA+
> ---------------------------------------------------------------------------------------------
>
> Key: HDDS-16432
> URL: https://issues.apache.org/jira/browse/HDDS-16432
> Project: Apache Ozone
> Issue Type: Sub-task
> Reporter: Siyao Meng
> Priority: Major
>
> Use TLA+ (via the Specula pipeline) to model and verify SCM HA follower catch
> up: the inter SCM checkpoint download and install during an apply window, the
> SCM HA transaction buffer flush versus durable index, and follower catch up
> after leader transfer. Model check the specification and validate real SCM
> traces against it. Bugs found by this effort are linked under this issue.
> Adjacent to HDDS-16141 (SCM delete-block) and HDDS-16079 (bootstrap
> checkpoint install).
> 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-ha-tx-buffer|medium|{{campaigns/ozone-9fbf9ee/targets/018-scm-ha-tx-buffer/.prompt-extra.md}}|1
> reproduced Critical, 1 masked Medium|
> |scm-follower-catchup|high|{{campaigns/ozone-9fbf9ee/targets/019-scm-follower-catchup/.prompt-extra.md}}|1
> masked Medium|
> 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, Critical) HDDS-16452: an InterSCMGrpcService.download
> checkpoint served during an apply window ships data at index i under the
> stale durable index i minus 1, so a follower installs it and durably holds
> data ahead of its recorded index. [scm-ha-tx-buffer MC-2]
> * (MASKED, Medium) HDDS-16453: an unguarded transaction buffer flush commits
> data under a stale index (DurableIndexMatchesData violated), masked by SCM
> idempotent replay, with divergence risk the moment a non idempotent
> replicated transaction is added. [scm-ha-tx-buffer MC-1]
> * (MASKED, Medium) HDDS-16454: a new SCM leader whose apply lags commit drops
> reports for committed but unapplied containers as CONTAINER_NOT_FOUND,
> leaving replica location accounting incomplete, masked by the WARN only
> default and replication manager readiness gating. [scm-follower-catchup MC-2]
> 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]
