hyhac VS shuttle

When I was writing a Haskell client library for Hyperdex, another distributed kv store, I found it incredibly helpful to implement a simulator for correctness. This helped me identify which behavior was unspecified (arithmetic overflow: should error) or where my simulator deviated.

https://github.com/AaronFriel/hyhac/blob/master/test/Test/Hy...

Alas, I think Hyperdex development paused a few years later. It's a shame that it stopped then.

This is what we did for our KV store at S3: https://www.amazon.science/publications/using-lightweight-fo...

Using https://github.com/awslabs/shuttle which works on our real Rust code.

They've also developed a library that plugs into their actual Rust code to verify it (rather than writing a secondary model in TLA+ or P, it's easier to verify the actual system source code).

See https://github.com/awslabs/shuttle and a whitepaper at https://www.amazon.science/publications/using-lightweight-fo...

Disclaimer: used to work at AWS and had some involvement in this stuff

loom and shuttle can help you narrow down the problem.

Loom is really awesome, though it is focused on exhaustive testing, so not suitable for code that has a lot of possible interleavings (e.g. due to a ton of threads, or a large body of code).

There is a new project out of AWS called Shuttle [1] which is like Loom, but it does random exploration instead of exhaustive exploration, which enables massively distributed testing of really complicated stuff.

[1] https://github.com/awslabs/shuttle