Notes on Black-box Isolation Checking with Elle a CMU database Quarantine Talk by Kyle Kingsburg

ELLE - a tool verify if a database is serializable or snapshot isolation level of a database.

This is a challenging thing to do.

How do you determine if a database is serialable?

We can have multiple actors do concurrent operations on a database and journal their results.

And then see if the order is legal.

The issue is that the number perumatations of legal transaction orders is very large (N!) so this technique does not work for large N.

The solution in 2015 was called Gretchen which implements a technique described by Cerone, Bernardi, & Gotsman 2015.

Rather the try to find all the orders lets break it into three catagories:

• Internal - Check in each trx separately.
• External - Build Read Dependancy Constraint problem in CNF (conjungive normal form)
• Total Visablity - Solve for order using integer constraint solver.

This is basically a SAT solver and is NP-Complete.

This technique is limited to ~100 txns. Doesn’t explain why no solution.