I'm pleased to announce Elle, a black-box, linear-time checker for transactional (or single-key!) consistency models. I've been working on this with @palvaro for over a year now. Now you can use it too!
http://arxiv.org/abs/2003.10554 http://github.com/jepsen-io/elle
-
-
Elle has been the secret behind most of the recent analyses on https://jepsen.io , and can automatically distinguish between read uncommitted, read committed, repeatable read, strict-1SR, etc. We believe it represents a novel and useful contribution to the field.
Show this thread -
If you have a background in Isabelle (or other proof systems), I'd appreciate your help in completing a formal proof of Elle's correctness. I've got most of the formalism and properties defined, but I'm stuck on lemmata. Interested? aphyr@jepsen.iohttps://github.com/jepsen-io/elle/tree/master/proof …
Show this thread
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.