[
https://issues.apache.org/jira/browse/HDDS-16141?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18125910#comment-18125910
]
Siyao Meng commented on HDDS-16141:
-----------------------------------
Verification run complete. The scm-delete-block target ran through the full
Specula pipeline at Ozone 9fbf9ee0cb1bd2f5f5d437b6719ebbe5309351fb
(claude-code, Claude Opus 4.8, effort max).
h3. Result
Eight findings came out of model checking (5) and code review (3).
||Finding||Disposition||Issue||
|MC-2|Reproduced, Medium|HDDS-16142|
|MC-3|Reproduced, Medium|HDDS-16143|
|MC-4|Env limited, High|HDDS-16144|
|MC-5|Reproduced, Medium|HDDS-16145|
|MC-1|Env limited, High|Not filed|
|CR-1|Masked, Medium|Not filed|
|CR-2, CR-3|False positive|None|
h3. Not filed
* MC-1: the lock free {{recordTransactionCreated}} can recreate a
{{transactionToDNsCommitMap}} entry after its purge. The entry is cleared only
on leader failover, and the harm needs a very long leader term, which the unit
harness cannot produce.
* CR-1: a batched {{addTransactions}} leaves an earlier durable prefix when a
later batch fails. OM retry and idempotent DataNode deletion absorb it.
Resolving as Done.
> [Specula] Verify scm-delete-block (Apache Ozone master @9fbf9ee)
> ----------------------------------------------------------------
>
> Key: HDDS-16141
> URL: https://issues.apache.org/jira/browse/HDDS-16141
> 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 delete-block
> transaction protocol: deleted-block log durability, per-datanode command
> state, ACK and timeout handling, transaction retry and resend, replica-set
> membership at removal, the volatile deleted-block transaction summary
> accounting, and volatile-state reconstruction after SCM leader transfer,
> across the SCM HA transaction buffer and the durable RocksDB state.
> Model check the specification and validate real SCM traces against it. Bugs
> found by this effort are linked under this issue.
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
