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.

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.

If you're interested, email!

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.

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.

Show thread

Last fall, Replicache commissioned Jepsen to take a look at their design docs, and we wrote a bit about how it works:

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.


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