Uploaded image for project: 'Calcite'
  1. Calcite
  2. CALCITE-1977

Use Cosette to check whether planner rules are valid

    Details

    • Type: Bug
    • Status: Open
    • Priority: Major
    • Resolution: Unresolved
    • Affects Version/s: None
    • Fix Version/s: None
    • Component/s: None
    • Labels:
      None

      Description

      Use Cosette, an automated SQL solver from University of Washington, to check whether planner rules are valid.

      I don't know whether Cosette is written in Java, so the simplest approach might be to instrument the planner to generate a script. Suppose FilterProjectTransposeRule has just fired successfully. Then RelOptRuleCall#transformTo would generate the line

        assertEquivalent(
          "select * from (select empno from emp) where empno > 10",
          "select empno from (select * from emp where empno > 10)")
      

      (Those SQL statements are the result of converting the before and after RelNode instances to SQL.)

      We could run the Calcite test suite to produce a large script with probably thousands of those statements. Then the Cosette researchers can take that script and run it through Cosette (using whatever language they develop in). It would find bugs in Cosette (at first mostly deficiencies in Cosette's SQL parser, I fear) but also would find bugs in Calcite if the transformation is not valid. (Not too many, I hope!)

        Activity

        Hide
        michaelmior Michael Mior added a comment -

        Not written in Java, but Rosette (Racket) and Coq (Haskell). The easiest approach would probably be to just shell out to the tool. Also worth noting that it doesn't prove that rewrite rules are valid, but only that two queries are equivalent. So we could check that a particular rewrite is valid, but it doesn't necessarily mean that the rule is always correct.

        Show
        michaelmior Michael Mior added a comment - Not written in Java, but Rosette (Racket) and Coq (Haskell). The easiest approach would probably be to just shell out to the tool. Also worth noting that it doesn't prove that rewrite rules are valid, but only that two queries are equivalent. So we could check that a particular rewrite is valid, but it doesn't necessarily mean that the rule is always correct.
        Hide
        stechu Shumo Chu added a comment -

        Appreciate the discussion, Julian Hyde!

        Michael Mior Cosette author here. There are various ways of integrating Cosette. This easiest way is probably using [Cosette Web API](http://cosette.cs.washington.edu/guide#api). If you want to run everything locally, the easiest way is to build a Cosette docker and call the solver python API.

        Show
        stechu Shumo Chu added a comment - Appreciate the discussion, Julian Hyde ! Michael Mior Cosette author here. There are various ways of integrating Cosette. This easiest way is probably using [Cosette Web API] ( http://cosette.cs.washington.edu/guide#api ). If you want to run everything locally, the easiest way is to build a Cosette docker and call the solver python API.
        Hide
        julianhyde Julian Hyde added a comment -

        Or even easier, have Calcite generate a script. Cosette can be invoked offline.

        Show
        julianhyde Julian Hyde added a comment - Or even easier, have Calcite generate a script. Cosette can be invoked offline.

          People

          • Assignee:
            julianhyde Julian Hyde
            Reporter:
            julianhyde Julian Hyde
          • Votes:
            0 Vote for this issue
            Watchers:
            4 Start watching this issue

            Dates

            • Created:
              Updated:

              Development