Verifying Transactional Consistency with Jepsen and FaunaDB
1–10 of 27 posts
Re: Verifying Transactional Consistency with Jepsen and FaunaDB
#2Is this OSS?
> As part of our engineering process at Fauna, we have built a comprehensive suite of unit and property-based tests and as well as a sophisticated distributed testing framework that is capable of checking the behavior of FaunaDB in the presence of a wide combination of fault injections and operational changes, similar to Netflix’s Chaos Monkey.
What did you write your property testing framework in?
Re: Verifying Transactional Consistency with Jepsen and FaunaDB
#3Is this OSS? > As part of our engineering process at Fauna, we have built a comprehensive suite of unit and property-based tests and as well as a sophisticated distributed testing framework that is capable of checking the behavior of FaunaDB in the presence of a wide combination of fault injections and operational changes, similar to Netflix’s Chaos Monkey. What did you write your property testing framework in?
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.
Re: Verifying Transactional Consistency with Jepsen and FaunaDB
#4Jepsen is an important sanity check on marketing. Easy to say in collateral you are "strict" ACID -- Jepsen proves (or denies) those claims. Some fun reports over there http://jepsen.io/analyses
Re: Verifying Transactional Consistency with Jepsen and FaunaDB
#5How does fauna's consistency guarantees compare to coakroach, spanner and yugabyte? It is difficult to compare because different vendors use different terminology. For example spanner supports 'external consistency'. And Coakroach says it supports serializable as defined by ANSI. Is this the same as what Fauna calls strict serializable?
Re: Verifying Transactional Consistency with Jepsen and FaunaDB
#6Jepsen is an important sanity check on marketing. Easy to say in collateral you are "strict" ACID -- Jepsen proves (or denies) those claims. Some fun reports over there http://jepsen.io/analyses
"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
Re: Verifying Transactional Consistency with Jepsen and FaunaDB
#7Here is a direct link to the analysis: https://storage.pardot.com/517431/114459/FaunaDB_Correctness...
Re: Verifying Transactional Consistency with Jepsen and FaunaDB
#8Is this OSS? > As part of our engineering process at Fauna, we have built a comprehensive suite of unit and property-based tests and as well as a sophisticated distributed testing framework that is capable of checking the behavior of FaunaDB in the presence of a wide combination of fault injections and operational changes, similar to Netflix’s Chaos Monkey. What did you write your property testing framework in?
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 fa…
Would be good to see -- problems/issues that needed code fixes? maybe caused you to rethink (or regret) implementation decisions? I'm sure Kyle's report will have something good. I always root for Jepsen...and I haven't been disappointed yet.
Re: Verifying Transactional Consistency with Jepsen and FaunaDB
#9Jepsen is an important sanity check on marketing. Easy to say in collateral you are "strict" ACID -- Jepsen proves (or denies) those claims. Some fun reports over there http://jepsen.io/analyses
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?
Re: Verifying Transactional Consistency with Jepsen and FaunaDB
#10How does fauna's consistency guarantees compare to coakroach, spanner and yugabyte? It is difficult to compare because different vendors use different terminology. For example spanner supports 'external consistency'. And Coakroach says it supports serializable as defined by ANSI. Is this the same as what Fauna calls strict serializable?
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...