9,731 karma · joined January 15, 2010
Hacker, physics geek, clojurer, rubyist, aikidoist, photographer.
This is a wonderful idea, and I've got no idea how to actually do it in a standardized, rigorous way. Vendor claims are often contradictory, it's hard to get a good idea of anomaly frequency, availability is... a rabbithole, and it's hard to come up with a standard taxonomy of anomalies--most of the analyses I do wind up finding something I've never really seen before, haha. With that in mind, I've wound up letting the reports speak for themselves.
Also, ideally the analyses should be rerun automatically (or possibly after being paid, but making it easy for the company to do so) every time a new major release happens rather than being done once and then being stale.
I don't know a good way to do this either. Each report is typically the product of months of experimental work; it's not like Jepsen is a pass-fail test suite that gives immediately accurate results. There is, unfortunately, a lot of subtle interpretive work that goes into figuring out if a test is doing something meaningful, and a lot of that work needs to be repeated on each test run. Think, like... staring at the logs and noticing that a certain class of exception is being caught more often than you might have expected, and realizing that a certain type of transaction now triggers a new conflict detection mechanism which causes higher probabilities of aborts; those aborts reduce the frequency with which you can observe database state, allowing a race condition to go un-noticed. That kinda thing.
If I'm lucky and the API/setup process haven't changed, I can re-run an analysis in about a week or so. If I'm unlucky, there's been drift in the OS, setup process, APIs, client libraries, error handling, etc. It's not uncommon for a repeat analysis to take months. :-(
I am delighted to say that yes: checking safety properties of distributed systems, including those of relational databases, is literally my job. See https://jepsen.io/analyses for a comprehensive list of prior work, or http://jepsen.io/analyses/tidb-2.1.7, http://jepsen.io/analyses/yugabyte-db-1.1.9, http://jepsen.io/analyses/yugabyte-db-1.3.1, or http://jepsen.io/analyses/voltdb-6-3 for recent examples of Jepsen analyses on relational databases.
This anomaly occurred even with read concern snapshot and write concern majority
3.5: In this case, a test running with read concern snapshot and write concern majority executed a trio of transactions with the following dependency graph
3.6: Worse yet, transactions running with the strongest isolation levels can exhibit G1c: cyclic information flow.
3.7: It’s even possible for a single transaction to observe its own future effects. In this test run, four transactions, all executed at read concern snapshot and write concern majority, append 1, 2, 3, and 4 to key 586—but the transaction which wrote 1 observed [1 2 3 4] before it appended 1.
Like... if you had read any of these sections--or even their very first sentences--you wouldn't be in this position. They're also summarized both in the abstract and discussion sections, in case you skipped the results.
4.0: Finally, even with the strongest levels of read and write concern for both single-document and transactional operations, we observed cases of G-single (read skew), G1c (cyclic information flow), duplicated writes, and a sort of retrocausal internal consistency anomaly: within a single transaction, reads could observe that transaction’s own writes from the future. MongoDB appears to allow transactions to both observe and not observe prior transactions, and to observe one another’s writes. A single write could be applied multiple times, suggesting an error in MongoDB’s automatic retry mechanism. All of these behaviors are incompatible with MongoDB’s claims of snapshot isolation.
It's OK to stop digging now!
May I suggest sections 3.4, 3.5, 3.6, 3.7, 4.0, and 4.1?
Jepsen draws inspiration from a long line of work on property-based testing, especially Quickcheck & co. It also draws on roughly 10 years of experience building & running distributed systems in production. A lot of Jepsen I invented from whole cloth, but some of the checkers in Jepsen are derived from specific research papers, like work by Wing, Gong, and Howe on linearizability checking.
Then it's just... a lot of thinking, experimenting, and writing. Jepsen's the product of ~6 years of full-time work. Elle, the system which detected the anomalies in this report, was a research project I've been puzzling over for roughly two years.
I write the Jepsen series, and open-source all of the code for these tests, partly as a resource so that other people can learn to do this same kind of work. :-)
Gently, may I suggest that you read the report, or at least the abstract? This is addressed in the second sentence. :-)
I'm also excited about my own research with Elle, but we're still working on getting that through peer review, haha. ;-)
The middle part of the report talks about unexpected but (almost all) documented behavior around read and write concern for transactions. I don't want to conjecture too much about motivations here, but based on my professional experience with a few dozen databases, and surveys of colleagues, I termed it "surprising". The fact that there's explicit documentation for what I'd consider Counterintuitive API Design suggests that this is something MongoDB engineers considered, and possibly debated, internally.
The final part of the report talks about what I'm pretty sure are bugs. I'm strongly suspicious of the retry mechanism: it's possible that an idempotency token doesn't exist, isn't properly used, or that MongoDB's client or server layers are improperly interpreting an indeterminate failure as a determinate one. It seems possible that all 4 phenomena we observed stem from the retry mechanism, but as discussed in the report, it's not entirely clear that's the case.
MongoDB's also published a writeup (which is cited a few times in the Jepsen report!) talking about the impact of stronger safety settings and why they choose weak defaults: http://www.vldb.org/pvldb/vol12/p2071-schultz.pdf
That's not to say that workarounds don't exist, just that I didn't find any in the documentation or by twiddling config flags in the ~2 weeks I was working on this report. :)
https://jepsen.io/analyses/mongodb-4.2.6
... and the corresponding HN thread here:
> Those can be done concurrently if at the same query level, so not necessarily any slower.
An important clarification, yes! I should have made that more explicit. :)
For simulation testing, I'd suggest looking at Maelstrom, which uses Jepsen to provide a sort of workbench for writing toy Raft implementations in any language. You give it a binary which takes messages as JSON on STDIN and emits messages to STDOUT; it spawns a bunch of "nodes" (local processes) of that binary, connects them via a simulated network, generates pathological network behavior, simulates client requests, and verifies the resulting histories with Jepsen.
Also keep in mind that typical Dgraph workloads request specific attributes (think "SELECT NAME, AGE") rather than everything ("SELECT *"), which reduces the impact of fanout. :)
https://github.com/jepsen-io https://jepsen.io/ https://jepsen.io/ethics
Consider RandDB, a database which returns random values for reads. It is possible that with RandDB, we happen to get a history which looks, say, serializable. And indeed, the observed history might be equivalent to a serializable Adya history, even though the underlying system is clearly not. This is, however, an accident--and given sufficiently long histories, the probability that we fail to observe a violation decreases.
Another possibility is that a database can explode the state space by producing indeterminate results for transactions. Of course, a database that deliberately did this would be silly, because nobody wants (I assume!?) a database that throws errors constantly. But when indeterminacy does happen, it's possible that we might fail to resolve some underlying anomaly. For instance, say an indeterminate write transaction actually aborts internally, but we don't know it aborted. If a committed read sees that write, that's technically an aborted read, but Elle (or any external observer) wouldn't be able to tell, because we can't prove the original write transaction aborted.
Likewise, if a database happens to avoid returning reads for some writes, we can't say anything about what write orderings are illegal. In the case of list append, we have the nice property that any single read tells us the entire version history up to that read, so the fraction of the version order we can't infer is limited to some (hopefully) short series of writes in the last n seconds. If the database never returns a read, though, all bets are off!
While this is on frontpage, I'd like to ask: if anyone has experience with machine proofs, I'd appreciate your help in completing a formal proof of Elle's correctness. I've been teaching myself Isabelle/HOL in an attempt to formalize the proof sketch, and I have encoded most of the formalism and properties I care about, but actually proving lemmata has been... frustrating. Like, I burned hours one one lemma because it hinged on showing \forall x :: Nat, x \in N.
https://github.com/jepsen-io/elle/tree/master/proof
If you'd like to work on this, my email is aphyr@jepsen.io!