aphyr

Well... it's not quite so straightforward. SI still allows some phantoms. It only prohibits some of them.

In PostgreSQL's case, if they somehow made repeatable read to prevent G2-item without sacrificing the phantom reads, would that mean repeatable read is then "serializable" according to the ANSI definition?

I'm not quite sure I follow--If you're asking whether snapshot isolation (Postgres "Repeatable Read") plus preventing G2-item is serializable, the answer is no--that model would still allow G2 in general--specifically, cycles involving non-adjacent rw dependencies with predicates.

Jokes aside, Marklogic is welcome to pay me. Each one of these reports takes weeks to months of full-time work.

The ANSI definitions are bad: they allow multiple interpretations with varying results. 25 years ago, Berenson, O'Neil, et al. published a paper showing the ANSI definitions had this ambiguity, and that what the spec meant to define should have been a broader class of anomalies. They literally say that the broad interpretation is the "correct" one, and the research community basically went "oh, yeah, you're right". Adya followed up with generalized isolation level definitions, and pretty much every paper I've read has gone with these versions since. That didn't make its way back into the SQL spec though: it's still ambiguous, which means you can interpret RR as allowing G2-item.

Why prevent G2-item in RR? Because then the difference between repeatable read and serializable is specifically phantoms, rather than phantoms plus... some other hard-to-describe anomalies. If you use the broad/generalized interpretation, you can trust that a program which only accesses data by primary key, running under repeatable read, is actually serializable. That's a powerful, intuitive constraint. If you use the strict interpretation, RR allows Other Weird Behaviors, and it's harder to prove an execution is correct.

For a very thorough discussion of this, see either Berenson or Adya's papers, linked throughout the report.

That said, I've found core.typed helpful in managing complex state transformations, especially in namespaces which have, say, five or six similar representations of the same logical thing. What do you do when a "node" is a hostname, a logical identifier in Jepsen, an identifier in the database itself, a UID, and a UID+signature pair? Managing those names can be tricky, and having a type system really helps.

I've considered spec as well, but spec has a weird insistence that a keyword has exactly one meaning in a given namespace, which is emphatically not the case in pretty much any code I've tried to verify. Also its errors are... not exactly helpful.

If you look at Elle's transaction generators, you can cap the size of any individual key, and use an uneven (e.g. exponential) distribution of key choices to get various frequencies. That way keys stay reasonably small (I use 1-10K writes/key), some keys are updated frequently to catch race conditions, and others last hundreds of seconds to catch long-lasting errors.

So I'm curios how would you have described the ability of finding violations with Elle using read-write registers with unique values vs the append-only lists?

RW registers are significantly weaker, though I don't know how to quantify the difference. I've still caught errors with registers, but the grounds for inferring anomalies are a.) less powerful and b.) can only be applied in certain circumstances--we talk about some of these details in the paper.

This is based on her presentation and some dinner conversation at HPTS 2019, so I don't know if there's actually a paper I can point to. The gist of is that Paxos normally involves an arbitration phase where there are conflicting proposals, which adds a second pair of message delays. But if you relax the consensus problem to agreement on a set of proposals, rather than a single proposal, you don't need the arbitration phase. Instead of "who won", it becomes "everyone wins". Then you can impose an order on that set via, say, sorting, and iterate to get a replicated log.

I read over bits of Elle; the documentation in it is absolutely top-notch. You and Peter Alvaro knocked it out of the park!

Thank you! Could I... hang on, just let me grab reviewer #1 quickly, I'd like them to hear this. ;-)

"Why don't you put Jepsen:" on the same line as the database name and version?"

Space concerns, and also, it's immediately above the DB name in giant letters.

"Why don't you give them more creative names?"

Clients love to argue about the titles of these analyses; having a concise, predictable policy for titling is how I get past those discussions.