Summary

Extend the model-based test framework (test/model) to validate asynchronous step-down workflows, ensuring correctness of concurrent transactions and timestamp semantics across step-down events.

Motivation

The model framework provides lightweight formal verification of WiredTiger's transactional and timestamp behaviors. Adding async step-down scenarios to test/model ensures the correctness properties (visibility, ordering, durability) are verified at a formal level, complementing the functional coverage added in WT-17897.

Scope

• Model-based tests for concurrent operations (reads/writes) transitioning during an async step-down event
• Verification of timestamp semantics (commit, durable, read timestamps) across step-down
• Prepared transaction correctness during async step-down
• Stable/unstable visibility invariants across step-down transitions

Definition of Done

• test/model tests cover async step-down with:
  • Concurrent read/write operations
  • Timestamp correctness (commit, durable, read timestamps)
  • Prepared transaction workflows
  • Stable timestamp visibility invariants