Implementation and Synthesis of Math Library FunctionsDistinguished Paper
Achieving speed and accuracy for math library functions like exp, sin, and log is difficult. This is because low-level implementation languages like C do not help math library developers catch mathematical errors, build implementations incrementally, or separate high-level and low-level decision making. This ultimately puts development of such functions out of reach for all but the most experienced experts. To address this, we introduce MegaLibm, a domain-specific language for implementing, testing, and tuning math library implementations. MegaLibm is safe, modular, and tunable. Implementations in MegaLibm can automatically detect mathematical mistakes like sign flips via semantic well-formedness checks, and components like range reductions can be implemented in a modular, composable way, simplifying implementations. Once the high-level algorithm is done, tuning parameters like working precisions and evaluation schemes can be adjusted through orthogonal tuning parameters to achieve the desired speed and accuracy. MegaLibm also enables math library developers to work interactively, compiling, testing, and tuning their implementations and invoking tools like Sollya and type-directed synthesis to complete components and synthesize entire implementations. MegaLibm can express 8 state-of-the-art math library implementations with comparable speed and accuracy to the original C code, and can synthesize 5 variations and 3 from-scratch implementations with minimal guidance.
Wed 17 JanDisplayed time zone: London change
10:30 - 11:50 | |||
10:30 20mTalk | Implementation and Synthesis of Math Library FunctionsDistinguished Paper POPL | ||
10:50 20mTalk | Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations POPL | ||
11:10 20mTalk | Efficient Bottom-Up Synthesis for Programs with Local Variables POPL Xiang Li University of Michigan, Ann Arbor, Xiangyu Zhou University of Michigan, Rui Dong University of Michigan, Yihong Zhang University of Washington, Xinyu Wang University of Michigan Pre-print | ||
11:30 20mTalk | Optimal Program Synthesis via Abstract Interpretation POPL Stephen Mell University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Osbert Bastani University of Pennsylvania |