Solitaire is a faster Linearizability checker supporting multi-interface.
Given a concurrent history, Solitaire will determine whether the history is Linearizability by finding a sequential specification. The basic algorithm is described in Faster linearizability checking via P-compositionality.
Solitaire is named after the famous Windows card game, which involve dealing cards from a shuffled deck into a prescribed arrangement on a tabletop.
# Compile
cd kv_checker
g++ -std=c++11 -O2 kv_checker.cc sl_op_kv.cc ../src/sl_checker.cc ../src/sl_cache.cc -I.. -o kv_checker
# Run
kv_checker test/test_demo.txt
- Optimize bitset hash
- Support Multi-thread