reOiL/whirl-matrix

whirl-framework/whirl-matrix mirror

Whirl-Matrix

Deterministic simulator for Whirl

Example

KV – simple replicated KV store

• Quorum reads / writes
• Timestamp ordering via wall clocks

Note: this implementation intentionally violates linearizability!

Use Attiya, Bar-Noy, Dolev (ABD) algorithm for linearizable behaviour:

• Original paper
• Notes on Theory of Distributed Systems – Chapter 16 – Distributed Shared Memory

Features

• Determinism (concurrency, time, network, randomness)
• Time compression
• Linearizability checker
• Persistence (via filesystem) and node restarts
• Local clock skew and drift
• Google TrueTime simulation
• Pluggable asynchrony and fault injection strategy

Inspiration

Simulation + Fault Injection

FoundationDB

• Testing Distributed Systems w/ Deterministic Simulation
• FoundationDB or: How I Learned to Stop Worrying and Trust the Database

AWS

• Millions of Tiny Databases

Jepsen

• https://github.com/jepsen-io/maelstrom

Paxi

• Dissecting the Performance of Strongly-Consistent Replication Protocols
• https://github.com/ailidani/paxi

Model checking

Microsoft Coyote

• https://microsoft.github.io/coyote
• https://github.com/microsoft/coyote

DSLabs

• Teaching Rigorous Distributed Systems With Efficient Model Checking
• https://github.com/emichael/dslabs

StateRight

• https://github.com/stateright/stateright

Fuzzing

• Fuzzing Raft for Fun and Publication
• Minimizing Faulty Executions of Distributed Systems

Requirements

• x86-64
• Linux or MacOS
• Clang++ (>= 10.0)

Build

# Clone repo
git clone https://gitlab.com/whirl-framework/whirl-matrix.git 
cd whirl-matrix
# Generate build files
mkdir build && cd build
cmake -DWHIRL_MATRIX_EXAMPLES=ON ..
# Build kv example
make whirl_example_kv
# Run kv example
# --det - run determinism check
# --sims - number of simulations to run
./examples/kv/whirl_example_kv --det --sims 12345