5 ms·

Why?

BrentOzar 9y ago
Because it's a lot of work tuning complex SQL queries, and you can easily make a coding mistake that runs faster - but produces different results.
- jzelinskie 9y ago
  I'm assuming this solver only works on a particular subset of SQL like ANSI SQL. Applications are often coupled to one database by using exotic features and non-portable SQL. In fact, the more you need performance, the more likely you are to leverage these aspects of your database and prevent yourself from using a tool like this.
parshimers 9y ago
Because it's awesome! You've never had to rewrite a query for some sort of reason other than the results returned (e.g. performance) and really wondered if the original and rewritten query were exactly the same?
- infogulch 9y ago
  I ended up building some tooling scripts to do this for stored procedures. It compares the output of the current and proposed stored procedures for all possible parameters and displays the differences and the set of parameters that it used. It's not formal verification by any means, but it seemed to work pretty well in practice. It would take forever though. I'd start it and walk away for a couple hours when I wanted a thorough test. But my confidence in correctness and performance gain (it measured perf too) was well worth the effort.
akc2 9y ago
also, no need to write test cases again if they can prove or disprove two queries.
- mulmen 9y ago
  You still need test cases to make sure the requirements have been satisfied. Even in the case where you know there is a problem with a query and show there is a difference with Cosette there is no guarantee that it will show the specific difference you are looking for. This is a fantastic tool but it doesn't replace testing.
  - akc2 9y ago
    fair enough. I was thinking more on the side of "this rewrite should be correct and indeed it is" by asking the tool to come up with a proof rather than doing extensive testing.
    - mulmen 9y ago
      Cosette can prove equivalency but not correctness. Unit testing can't prove correctness either but it can demonstrate that specific conditions are satisfied. If you have a query 1 that satisfies case a and b but then identify a bug and add case c you can write a query 2 which satisfies a, b and c and indeed Cosette may identify that case as the difference (or not!) but you still have no guarantee that you will not then discover case d which is not satisfied by 1 or 2 or a future 3.
    - deleted 9y ago
      [deleted]
    - ams6110 9y ago
      Even if the two queries are provably equivalent, that does not mean that the database engine will produce the same results for the two. There could be bugs in the implementation.
edejong 9y ago
Most of all, because if you can prove that two queries are equivalent in behavior, you are close to proving that one DBMS has the same behavior as another DBMS for all possible SQL queries. And then you ask: Why? Well, if you can prove two DBMSs equal for all SQL queries, you can prove that an optimization to the DBMS (such as an improvement to the query optimizer or new indexing systems) will not affect the behavior of any possible SQL you provide.
- DasIch 9y ago
  That's not at all what this does and it's not possible to do either.
  - heng222 9y ago
    It'll be possible if both databases are written using proof assistants like Coq. And I think this work is a step towards that direction.
  - edejong 9y ago
    That's what you can do with Coq. I can implement a reference interpreter and an optimized compiler and prove that the behavior of all possible programs are equivalent in both environments. This is, what I assume, the long-term target of the article.
    - DasIch 9y ago
      You'd need to prove that a DBMS executes a query always correctly to begin with. That in itself would be quite the task. Additionally SQL as supported by some DBMSes (e.g. Postgres due to recursive CTE and window functions) is turing complete. That makes proving equivalency in general a bit challenging.
Scotrix 9y ago
Thanks for the explanation guys. I totally forgot that there is something like SQL tuning and optimising.

Why?

Because it's a lot of work tuning complex SQL queries, and you can easily make a coding mistake that runs faster - but produces different results.

jzelinskie 9y ago
I'm assuming this solver only works on a particular subset of SQL like ANSI SQL. Applications are often coupled to one database by using exotic features and non-portable SQL. In fact, the more you need performance, the more likely you are to leverage these aspects of your database and prevent yourself from using a tool like this.

parshimers 9y ago

Because it's awesome! You've never had to rewrite a query for some sort of reason other than the results returned (e.g. performance) and really wondered if the original and rewritten query were exactly the same?

infogulch 9y ago
I ended up building some tooling scripts to do this for stored procedures. It compares the output of the current and proposed stored procedures for all possible parameters and displays the differences and the set of parameters that it used. It's not formal verification by any means, but it seemed to work pretty well in practice. It would take forever though. I'd start it and walk away for a couple hours when I wanted a thorough test. But my confidence in correctness and performance gain (it measured perf too) was well worth the effort.

akc2 9y ago

also, no need to write test cases again if they can prove or disprove two queries.

mulmen 9y ago
You still need test cases to make sure the requirements have been satisfied. Even in the case where you know there is a problem with a query and show there is a difference with Cosette there is no guarantee that it will show the specific difference you are looking for. This is a fantastic tool but it doesn't replace testing.
- akc2 9y ago
  fair enough. I was thinking more on the side of "this rewrite should be correct and indeed it is" by asking the tool to come up with a proof rather than doing extensive testing.
  - mulmen 9y ago
    Cosette can prove equivalency but not correctness. Unit testing can't prove correctness either but it can demonstrate that specific conditions are satisfied. If you have a query 1 that satisfies case a and b but then identify a bug and add case c you can write a query 2 which satisfies a, b and c and indeed Cosette may identify that case as the difference (or not!) but you still have no guarantee that you will not then discover case d which is not satisfied by 1 or 2 or a future 3.
  - deleted 9y ago
    [deleted]
  - ams6110 9y ago
    Even if the two queries are provably equivalent, that does not mean that the database engine will produce the same results for the two. There could be bugs in the implementation.

edejong 9y ago

Most of all, because if you can prove that two queries are equivalent in behavior, you are close to proving that one DBMS has the same behavior as another DBMS for all possible SQL queries. And then you ask: Why? Well, if you can prove two DBMSs equal for all SQL queries, you can prove that an optimization to the DBMS (such as an improvement to the query optimizer or new indexing systems) will not affect the behavior of any possible SQL you provide.

DasIch 9y ago
That's not at all what this does and it's not possible to do either.
- heng222 9y ago
  It'll be possible if both databases are written using proof assistants like Coq. And I think this work is a step towards that direction.
- edejong 9y ago
  That's what you can do with Coq. I can implement a reference interpreter and an optimized compiler and prove that the behavior of all possible programs are equivalent in both environments. This is, what I assume, the long-term target of the article.
  - DasIch 9y ago
    You'd need to prove that a DBMS executes a query always correctly to begin with. That in itself would be quite the task. Additionally SQL as supported by some DBMSes (e.g. Postgres due to recursive CTE and window functions) is turing complete. That makes proving equivalency in general a bit challenging.

Scotrix 9y ago

Thanks for the explanation guys. I totally forgot that there is something like SQL tuning and optimising.