Elle: Inferring Isolation Anomalies from Experimental Observations
arxiv.org
arxiv.org
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 had a question about your completeness argument (in 4.3.1), you say "we typically observe enough of a history to detect the presence of non-cycle anomalies". I think I understood why that is after reading the rest of the paper, but I didn't understand the worst case. Is it possible, for example, for a database to intentionally construct incorrect histories that Elle doesn't detect?
I don't have any real "evil database" threat model in mind, just trying to test my understanding.
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!