Skip to content

Meeting Notes

Jump to bottom Edit New page
James Wilcox edited this page Jan 28, 2014 · 10 revisions

14-01-27 @ 4:30pm

  • Talked about the history of changes on each rule
    • Current implementation gives the input expression and the output expression for each rule
    • Might be better to have the name of the rule and the bindings.
  • Discussed POPL -Might be possible to take benchmarks from Darulova et al. -Should be easy to improve on some of their implementations
  • Discussed Mark (met at POPL) who wants to work on the same problem
    • Resolved: talk to Zach about it
  • Errors becoming a list, not the max-error
    • Probably want summaries anyway
    • The exp example no longer strictly improves with the "correct" version
    • The old version is better for large negative numbers (NaN v. 0)
    • Inferring regime changes should be possible now
  • Talked about red/green strategy
    • What should "green" mean in the context of the errors at each point
    • Is being worse at one point sufficient to be not green? If not, how many is too many?
    • Which steps should be "green"? (1 + x) - x) → 1 + (x - x) is clearly green, but the inversion on the square root example is not.
  • Talked about focusing
    • Right now, the focusing is separate from the brute-force search
    • It'd be nice to have some sort of top-level driver that decided when to focus, when to brute-force, and would keep track of the "green" versions of a program.
  • Talked about representing rules
    • We want an explicit representation of rules
    • This lets us get a list of bindings
    • We'll need to write our own pattern matcher for that, it looks like
    • We can also compute how a pattern match transforms locations
    • For example, (a + b) + c → a + (b + c) changes the path into b from (1 2 …) to (2 1 …)
    • Also, representing locations as indices instead of car/cdr pairs might be good. Then again, maybe not.

13-11-06 @ 10:30am

  • Pavel added cost modeling to help guide search
  • A couple new ideas
    • introducing branches to allow for different regimes.
      • how to generate branch expression?
    • what would we need to generate kahan summation?
      • keep it simple: new mode for functions folded over a list
      • rewrite rule to generate the body of the loop
  • New/more sources of benchmarks
    • James to type up some stuff from Hamming
    • Akshay to put in some logistic regression stuff
    • Ask ML students for code?
    • Talk to Carlos/other faculty with examples?

13-10-30 @ 10:30am

Pavel prototype pretty sweet for our one example.

Need more diversity in synthesizer.

Guide by benchmarks drawn from:

13-10-25 @ 9:30am

2D conceptual framework:

  • (A) equiv over R vs. (B) float error reduced
  • A handled by CAS, B seems harder
  • prove equivalence over the reals?
  • yes
    • prove error over floats reduced?
    • yes
      • does no harm
      • most demanding case
      • probably produce slowest code
      • for critical software
    • no
      • more aggressive error optimization
      • result "correct" over reals... but who cares?
      • perhaps this case makes least sense?
      • how to eval? who is this for?
  • no
    • prove error over floats reduced?
    • yes
      • so non-equiv real, but better error wrt to spec for float
      • seems weird! lets us use stuff that "works" but we can't prove
        • Akshay's complex differentiation trick
        • taylor series expansion
      • still appropriate for critical software?
    • no
      • best effort
      • should produce fastest code (?)
      • how to eval? *why not just make every program "0.0"?

We should shoot for (Yes, Yes) -- proving equivalent over reals and proving the error is reduced, then we relax constraints to explore full space.

Need to consider "bigfloats" and continued fractions. Why wouldn't programmer just use these? Presumably efficiency. Need to consider this when asking who tool is for. How do we eval vs. these?

What about float optimizations in GCC? Can we help there?

  • historically, gcc has screwed this up with associativity
  • seems harder dealing with arbitrary code from the wild
  • ensure not using SSE when error is important?
  • drop doubles to floats when error doesn't matter?

Example analysis:

  (e^x - 1)/x
vs.
  let y = e^x in (y - 1)/log(y)

We can generate code which depends on dynamic properties

  • test for which regime this run is in
  • use version of the program most robust for this run
  • e.g. quadratic equation, if(abs(a-c) < N) { QE1 } else { QE2 }

Related work:

TODO

Prototype pattern matcher to search through equiv exprs over reals

Add a custom footer
Add a custom sidebar
Clone this wiki locally