Verifying Transactional Consistency with Jepsen and FaunaDB

We run FaunaDB as a service, or you can license it for on-prem use. Drivers and tooling are all open however, and we plan to release the source for correctness testing as well.

Our property tests are written in Scala as a Monad for controlling execution and random sample generation, and our internal distributed test harness uses Akka. This worked out nicely because we were able to make the relevant integration and fault tests scale from local runs via SBT to full geo-distributed clusters and OS-level fault injection.

Some conversation on CockroachDB vs FaunaDB here - https://news.ycombinator.com/item?id=16878102

The primary difference is in the interface (SQL vs NoSQL), the transactional protocol, and capabilities such as built-in multi-tenancy, temporality..

Might be useful to note that GV invested in both (Fauna was after Cockroach).

A bit more precisely: Jepsen denies or doesn't a small subset of those claims.

It can't prove strict acid because it only observes behaviour it can observe. There are code paths it won't see in practice, so the best it can do is refute.

It also can't refute acid as a whole. If you look at the reports, they usually check the very basic behaviour - simple sets and gets. While that can tell you a lot about the system, you can't say it will generalise to complicated joins, multi-row operations, backend plugins, etc.

I would also say "strict" ACID is become just another marketing term. I think what is more important is evaluating a databases support of different consistency and isolation levels. As well what level of availability do they support with these transaction guarantees? Do they support fail over to an active replica on the fly with no downtime? Are minority replicas available during network partition?

"strict" ACID can mean a lot of different things. There is a lot of levels of consistency and they prevent different types of issues with data correction and isolation. I think database vendors should clarify what consistency model they mean as defined by https://jepsen.io/consistency

Not sure why building on FoundationDB is better than building on the similar internal storage foundations current vendors have already implemented?

I believe what we spanner calls 'external consistency' we call strict serializability. Read-write transactions in FaunaDB are strictly serializable, whereas reads default to serializable. This allows us to serve reads independently from the closest region to the client, cutting down on latency in geo-distributed clusters.

This is a bit weaker than external consistency or strict serializability; Peter Bailis has a good writeup on the meaning of serializability vs strict serializability here: http://www.bailis.org/blog/linearizability-versus-serializab...

It is a CP system, although reads scale out more similar to an AP system because coordination is not required on consistent reads.

This is a really important question.