> I did not find any proof of this in the rest of the report.
May I suggest sections 3.4, 3.5, 3.6, 3.7, 4.0, and 4.1?
9,565 karma · joined January 15, 2010
Hacker, physics geek, clojurer, rubyist, aikidoist, photographer.
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!
I don't think it would have helped: the Jepsen tests I wrote in 2014 only checked single-key gets, puts, and CaS operations; the problems we found in this report were in watches and locks.
When I applied for a policy, my agent provided me with an electronic signature pad at payment time. I understood that I was providing my consent to apply for coverage, and to pay for that policy. I do contract review as a part of my job, and read legal language carefully before signing.
Just before I left the building, they provided me with a folder full of informational material--a bunch of ads for state farm services and disability coverage in general, some policy overviews, etc. I set it on the counter when I got home, and planned to read it later--work was incredibly busy that week.
It turned out that State Farm had applied my payment signature to additional forms without my knowledge: a HIPAA authorization form and consent for State Farm to draw my blood and test it for HIV. I was provided neither verbal nor written information prior to signing that I was agreeing to either of these terms. I was not given a chance to review these agreements prior to signing. I didn't ask to see them, because I didn't know they were even a thing.
State Farm started pulling my health records from my old doctors. One of them thought it looked sketchy, and called me to confirm. My reaction was something like "What the fuck". They emailed me a copy of the forms, and that was the first time I learned I'd "agreed" to disclose my health records. Sure enough, they were in the folder: buried behind the ads and policy information. If I'd flipped through the folder in full before walking out the door, I could have run back in and insisted they cancel the authorization.
I immediately called State Farm, informed them they did not have my consent, and demanded they destroy any records they'd obtained. They said they'd do that. I've been waiting for them to confirm they've destroyed those records since, uh... May, I guess. The folder's still on top of my desk; I've been meaning to follow up with a HIPAA complaint. Started getting the state regulatory bodies involved, but haven't finished that process.
I had a detailed conversation with my agent at State Farm where we talked about the importance of informed consent and presenting people with paperwork prior to signing. He actually told me that not only was this standard procedure, but that he didn't actually know how to get a copy of the forms to show to customers so they could review before signing: the workflow State Farm designed didn't actually produce forms until the signature was already in place.
I don't fault my agent specifically for this; I fault State Farm's training and workflow. My understanding from talking with state regulators is that I'd have to initiate a complaint specifically against my agent, which is less than ideal. I like him and I don't want to fuck up his business, and he didn't understand that contracts require a meeting of the minds. This is, IMO, a systemic problem requiring better training and software design, and those are both State Farm corporate issues.