Jepsen 0.1.18 is now available, including support for cycle-detection tests with Elle, dumping packet captures with tcpdump, and quality-of-life improvements.

github.com/jepsen-io/jepsen/re

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've had a really difficult time convincing Isabelle of the lemmata.

github.com/jepsen-io/elle/tree

If you're interested, email aphyr@jepsen.io!

Jepsen boosted

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.

Show thread
Jepsen boosted

I'm pleased to announce the latest @jepsen project: Elle, a black-box, linear-time checker for transactional (or single-key!) consistency models. I've been working on this with Peter Alvaro for over a year now, and I'm delighted to finally have it out the door.

arxiv.org/abs/2003.10554

github.com/jepsen-io/elle

Elle has been the secret behind most of the recent Jepsen analyses, and we believe its techniques represent a novel and useful contribution to the field.

Again, this is just design review--I can't speak to anything about Replicache's implementation--but these properties are theoretically achievable! There's precedent in both Bayou and Eventually-Serializable Data Services, both from 1996! I'm kinda curious what kind of cross-pollination was going on there.

researchgate.net/publication/2

groups.csail.mit.edu/tds/paper

Show thread

Last fall, Replicache commissioned Jepsen to take a look at their design docs, and we wrote a bit about how it works: replicache.dev/jepsen.html.

They're doing something kinda like Bayou for mobile apps: local, speculative JS transactions, which are available even offline, replicated asynchronously. Those transactions may be reordered/re-executed with varying effects, but always preserve causal ordering; eventually they stabilize on a fixed serial order.

Hi Fediverse! You can follow this instance for Jepsen-related news--new analyses, project releases, etc.

Jepsen

A single-user Mastodon instance for Jepsen announcements & discussion.