percolator

TLA+ for Percolator.

# Check
java -XX:+UseParallelGC -Xmx12g -cp tla2tools.jar tlc2.TLC -workers auto spec.tla

This TLA+ model is of the percolator algorithm for implementing multi-row atomic transactions on top of a single-row atomic transaction system. See my blog post.

The failure model is crash stop or crash recover.