Thursday, July 7, 2011

synthesizing specialized hybrid value comparisons with Clojure metasketching


Recall that the hybrid value modifications in the backend extend the notion of a variable-value to be in four states:
  • A known constant (this was the only non-hybrid possibility before)
  • A value less than some bound
  • A value greater than some bound
  • An unknown value
    Things currently aren't very optimized. Suppose we have a variable x in the third state, i.e. we know x >= BND, where BND is some positive constant. Then, if we want to compute x > 0, we should return constant-true, not unknown. Similarly, if we multiply two large values, we should get another large value.

    There's a lot of these specialized functions -- one for every operator, and for every comparator we want to know whether it's possible, or known, that e.g. x > y, or whether is possible, denoted maybe. Instead of writing these core and critical specializations by hand, it would be nice to sketch them.
    So, first consider a known sketch generator. The sketch, marked by deffcn, takes two arguments, and checks whether these inputs being certain types of values (e.g. zero, large, unknown) will imply that the output is a certain type.

(defn known [xpred op ypred testpred]
  (test-hyp defaultopts (sketch
    (deffcn ^{:tag void :type harness} known-test [^int x ^int y]
      (defvar ^int opresult (op x y))
      (skassert (=> (and (xpred x) (ypred y)) (testpred opresult)))
    ))))

    The test-hyp will run the sketch, and return true if it succeeds, or false if it cannot be completed.

(defn test-hyp [opts prog]
  (def result (|> {:varGen (new TempVarGen) :prog prog}
    (semantic-check-stage opts true)
    (preproc-stage opts)
    (hack-lowlevelc opts)))
  (try
    (let [backend (new SATBackend opts rctrl (:varGen result))
           solns (seq (. backend partialEvalAndSolve (:prog result)))]
      true)
    (catch SketchNotResolvedException e false)) )

    Finally, to test out some hypotheses, we can call our sketch generator with various functions,

(defn isZero [x] (== 0 x))
(defn isHigh [x] (<= 10 x))
(defn isLow [x] (<= -10 x))
(defn test1 [] (known isHigh * isHigh isZero))
(defn test2 [] (known isLow * isHigh isLow))
(defn test3 [] (known isHigh * isHigh isHigh))

    The first test fails, since multiplying two high numbers doesn't always [in fact, ever, though that's not what we're testing for] result in zero. The second and third tests succeed, since they do always hold. Please check out skclojure1.clj in my branch (now clojurefe) if you're curious to see more.

No comments:

Post a Comment