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
-
Show this thread
-
Elle looks at histories of transactions from real databases, and infers constraints on version orders and the universe of all possible Adya-style dependency graphs consistent with that history. We employ cycle detection to automatically find and explain minimal anomalies.pic.twitter.com/FtN2nnx0rb
1 reply 4 retweets 33 likesShow this thread -
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.
4 replies 3 retweets 34 likesShow 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 …
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.