aphyr

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.

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!