Introducing Cosette

Today we are thrilled to announce our official 1.0 release of Cosette, a SQL solver for automatically checking semantic equivalences of SQL queries. With Cosette, one can easily verify the correctness of SQL rewrite rules, find errors in buggy SQL rewrites, building auto-graders for SQL assignments, developing SQL optimizers, busting “fake SQLs,” etc.

What is a SQL solver and what can it do?

As a SQL solver, Cosette checks for semantic equivalences of SQL queries. Two SQL queries are semantically equivalent if they produce the same results given any valid input relations. Here is an example of two semantically equivalent SQL queries:

These two queries will produce the exact same results no matter what the input relations r and s contain, and no matter what the predicate p is. So one can freely use one query for the other for any reason, e.g., improve query execution time, reduce amount of resources consumed, etc. Such rewrites form the basis of query optimization on modern database systems, such as MySQL, PostgreSQL, SQL Server, and [you name it], which all of us interact with (directly or indirectly) every day.

One would hope that all rewrites performed by database systems are indeed semantically preserving. Unfortunately, such rewrites are developed and checked by humans, and humans make mistakes. For example, can you decide if the following query Q3 is equivalent to the previous Q1?

Actually, they are not. We can show that Q3 is not equivalent to Q1 by the following counterexample:

Now let’s check the results of Q1 and Q3 running on this counterexample:

Thus Q1 and Q3 are not equivalent.

The core idea of Cosette is to automate this process: instead of reasoning about semantic equivalences manually, why not reason it using a computer program? Turns out that reasoning SQL equivalences is a two-fold problem. Given two SQL queries, Cosette will do the following:

1. If the two SQL queries are equivalent, Cosette will find a mechanical proof for the equivalence and validate it in using a Proof Assistant (currently Coq).
2. If the two SQL queries are inequivalent, Cosette will find a counterexample to show they are not equivalent. A counterexample is a set of specific input relation(s), where the two SQL queries will produce different results when executed using them, such as the one shown above.

There might be very complex cases where Cosette cannot decide the equivalences within time and computation resource limits. In such cases, Cosette will need help from users in order to finish the proof or come up with a counterexample.

Proving equivalences of SQL queries

Cosette proves the semantic equivalences of SQL queries by compiling them to machine checkable mathematical representations (called denotational semantics in programming languages research) and then using simple mathematical principles to reason about them. Let’s take a look at how Cosette compiles the queries above.

One basic concept in databases is relation (aka tables). A relation is just a bag of tuples, and being a bag means that the order of tuples doesn’t matter. What matters is how many times (also called multiplicity) a given tuple appears in a relation. Cosette borrows this idea from database theory and compiles relations to mathematical functions that, given a tuple, returns the multiplicity of it in the relation (this is formally called a K-Relation, after Green et al. PODS07). For example, let’s suppose relation r contains 3 tuples:

Notice that (“Alice”, 25) appears twice in the relation. Using the K-Relation representation, r(t1) = r(t2) = 2, and r(t3) = 1. For any other tuple t, we have r(t) = 0.

With this definition of a relation, a predicate is a function that returns either 0 or 1. For example, a predicate x = 1 returns 1 when applied to a tuple with attribute x equal to 1, or 0 otherwise. With all that in mind, a SQL query

is represented as

where t is a tuple.

Other SQL operators can be defined similarly. For example, the SQL bag union, union all, is simply defined as +, as the union of two bags means that the multiplicity of a tuple in the new relation is the sum of its multiplicities in the two input relations. Let’s look at the previous example:

Now here is the cool part: by using the distributivity of * and +, we can prove that Q1 is equivalent to Q2 since we can make them syntactically equivalent! This is how Cosette works internally. In addition, all the proofs are checked by a proof assistant called Coq. A proof assistant is a tool that checks the correctness of a proof mechanically. To learn more about how Coq (or proof assistants in general) works, check out this lengthy proof of the four color theorem, which is basically impossible to be check manually.

Finding counterexamples

You may ask, what if two SQL queries are not equivalent? We will never find a proof, right?

Indeed. However, since it might take a while (like, forever) for us to conclude that a proof doesn’t exist, it would be easier to show inequivalences by finding a counterexample. In Cosette, a counterexample is a set relations where the two queries will return different results when executed on them. Cosette search for such counterexamples using a SMT solver. The cool thing is, as a user, you don’t need to worry about how solvers work, since Cosette will compile SQL queries to the representations that a SMT solver can understand for you (just like how it compiles queries to K-Relations as shown above). Let’s look at an example. Assume you have two relations, parts with attributes pnum and qoh, and supply with attributes pnum and shipdate.

The above two queries were believed to be equivalent and were introduced as a clever rewrite rule in a database system in the 80’s. Three years afterwards, a researcher found that they are actually not equivalent , since Q5 ignores the empty groups.

While it took database researchers 3 years to realize and fix the problem, it only took Cosette fewer than 3 seconds to find a counterexample for the queries above:

The above shows the counterexample that Cosette found: supply as an empty relation and parts as a relation with only one tuple (pnum:0, qoh:0). You can try this example in our online demo (select “Example: Count Bug” from the dropdown menu) and you will realize how this is indeed a counterexample that shows the falsity of the rewrite rule.

Pretty cool, eh?

Learn and Use Cosette

Now that you understand how Cosette works, you can start using it by:

• Reading The Cosette Guide.
• Playing with Cosette online demo.
• Building your own applications using Cosette Web API.
• Subscribing to Cosette mailing list and following us on Twitter.
• Contributing to the project.

If you are a database researcher or hacker working on the next great SQL optimizer, get in touch with us to see how your system can become
“Cosette certified”!

This post was authored by Shumo Chu, Alvin Cheung, and Dan Suciu. We would like to thank Konstantin Weitz, Chenglong Wang, Daniel Li, and many other members from the database group and the programming languages and software engineering group at the University of Washington for their contributions and help.