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.
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 firstname.lastname@example.org!
A single-user Mastodon instance for Jepsen announcements & discussion.