-
Notifications
You must be signed in to change notification settings - Fork 41
Meeting Notes
wilcoxjay edited this page Oct 25, 2013
·
10 revisions
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:
- Zhendon Su POPL 13
- Kahan
- gotoblas
- atlas
- fftw (?)
Prototype pattern matcher to search through equiv exprs over reals