Verifying Global Consistency with Jepsen


Verifying Global Consistency with Jepsen

Today I’d like to give an update on our efforts to verify FaunaDB’s transactional correctness guarantees. In case you don’t know, FaunaDB is a mission critical, NoSQL database that guarantees data correctness in global environments without operational complexity. Most database technologies make you choose between productivity, scale and correctness. Instead, FaunaDB is scalable, ACID-compliant, multi-cloud, and highly available.

Our team has put in plenty of hard work to build in a distributed transaction engine, but not to be overlooked is the amount of work we have put into the infrastructure required for testing the system itself. We strongly believe that the only guarantees that a database system truly provides are those which are demonstrated to be valid. As part of our engineering process, we have built a comprehensive suite of unit and property-based tests, as well as a sophisticated distributed testing framework that is capable of checking the behavior of FaunaDB in the presence of a wide variety of cluster failure scenarios and configuration changes (and combinations thereof!).

I’m happy to report that we have also added Jepsen to the set of verification frameworks we are using to check our work. Kyle Kingsbury’s Jepsen has quickly earned a reputation as an industry standard suite for rigorously testing the capabilities and claims of distributed data systems.

We strongly believe that the only guarantees that a database system truly provides are those which are demonstrated to be valid.

Jepsen started with a simple question: How do systems behave in the presence of network failures? As we all found out via reading Kyle’s blog (and to many vendors’ chagrin), many systems showed significant flaws or failed to live up to their marketing claims. At Fauna, we stick with facts.

Jepsen has since become capable of simulating a much larger variety of hardware and cluster failure scenarios, and of checking a system’s more formal isolation characteristics, such as its ability to maintain sequential consistency, snapshot isolation, or linearizability in the presence of these failures.

Research has shown that the randomized testing methodology that Jepsen represents is effective at exposing bugs, especially faults related to partition tolerance. Therefore, we can have a high degree of confidence in a system’s ability to maintain correctness if it successfully passes a well-written set of tests based on randomized failure simulation.

Available now is a report of our preliminary testing results done recently by our own engineering team. In summary, what we found was that our efforts to build FaunaDB based on proven technology and in-hand with extensive testing and validation have paid off. So far, we have found no significant flaws in our implementation: FaunaDB is capable of preserving strong ACID guarantees in the face of concurrent operations, cluster reconfiguration, and faults.

Stay tuned for the independent analysis in the future, but in the meantime, have a look at our results .

An Invisible Tax on the Web: Video Codecs


Community Blog Round-Up: 11 July



Verifying Global Consistency with Jepsen