Using "Testing Shared Memories" paper to make linearizability checker faster on k/v stores with CAS

[Denis Rystsov]

Hi Jepsen users,

The "Testing Shared Memories" paper has an algorithm for testing linearizability with O(n ln n) complexity. I was playing with it a bit and managed to reproduce this analysis: https://aphyr.com/posts/322-call-me-maybe-mongodb-stale-reads, so the approach looks feasible :)

Reduced complexity allows to test systems for hours instead of minutes and check consistency claims during the long-running operations such as reconfiguration, compaction/vacuuming, splitting a single replica set into several shards, live update, taking backups etc.

Of course, the algorithm has some restrictions (e.g. all write operations must have a precondition) but they anyway arise naturally in a concurrent environment and don't limit the applicability.

The repo with detailed readme: https://github.com/rystsov/fast-jepsen

Cheers,

Denis

[Denis Rystsov]

Wow, I've just realized we can check linearizability even faster - O(n) instead of O(n ln n) :)

History is a zip of process-histories. Each process-history is sorted so if we group history by process id and do merge sort then we'll get sorted history. But there may be a lot of processes, so there is no guarantee that this sorting is more efficient than regular sorting. Fortunately, each process maps to a thread and a thread's time only goes forward so if we group history by thread we still get sorted thread-histories, and the amount of thread-histories is limited by (:concurrency test) which is low and independent from the length of the history.

I hope it will help to make tests more thoroughly. The repo is updated.

Cheers!