Distributed Systems Patterns
Common distributed-systems patterns as small, runnable formal specifications. Each page shows the spec, what the model checker verifies, and the expected result. For in-depth, step-by-step walkthroughs, see the examples.
- Mutex Pattern: Simple mutual exclusion with lock/unlock.
- Read-Write Lock Pattern: Multiple readers OR single writer.
- Distributed Lock Pattern: Multiple clients competing for lock with lease expiration.
- Optimistic Locking Pattern: Version-based concurrency control.
- Two-Phase Commit Protocol (walkthrough): Distributed transaction coordination with roles.
- Saga Pattern: Long-running transaction with compensation.
- Snapshot Isolation Pattern: Transactions read from snapshot, commit if no conflicts.
- Consensus Pattern (walkthrough): Simple consensus with proposals and acceptance.
- Leader Election (Simplified Raft): Distributed leader election with term-based voting.
- Compare-And-Swap Pattern: Atomic compare-and-swap for lock-free algorithms.
- Producer-Consumer Pattern: Classic bounded buffer problem.
- Message Queue Pattern: Distributed message queue with multiple producers and consumers.
- Cache Coherence Pattern: Simple write-through cache with invalidation.
- Eventual Consistency Pattern: Primary-replica replication with eventual convergence.
- Idempotent Operations Pattern: Operations that can be safely retried.
- Circuit Breaker Pattern: Prevents cascading failures with circuit states.
- Rate Limiting Pattern: Token bucket rate limiter.
- Write-Ahead Log Pattern: Durability through logging before applying changes.
- Event Sourcing Pattern: State derived from event stream.