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
-
-
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 threadThanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
I would really love an implementation-focused blog post version of the paper, as I’m struggling to derive “how do I implement this” through the theory-focused view the paper presents.
-
There's a whole reference implementation that you can read or, if you just want to use Elle, call directly from any JVM program, or shell out to. Having written it, it's both... an engaging problem, and also a whole enormous ball of worms which will eat up months of your life.
End of conversation
New conversation -
-
-
outstanding
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
Congrats! It’s a significant step forward. I am looking forward to seeing more of it in your analyses.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.