Probability type inference for flexible approximate programming
- 23 October 2015
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
Abstract
In approximate computing, programs gain efficiency by allowing occasional errors. Controlling the probabilistic effects of this approximation remains a key challenge. We propose a new approach where programmers use a type system to communicate high-level constraints on the degree of approximation. A combination of type inference, code specialization, and optional dynamic tracking makes the system expressive and convenient. The core type system captures the probability that each operation exhibits an error and bounds the probability that each expression deviates from its correct value. Solver-aided type inference lets the programmer specify the correctness probability on only some variables—program outputs, for example—and automatically fills in other types to meet these specifications. An optional dynamic type helps cope with complex run-time behavior where static approaches are insufficient. Together, these features interact to yield a high degree of programmer control while offering a strong soundness guarantee. We use existing approximate-computing benchmarks to show how our language, DECAF, maintains a low annotation burden. Our constraint-based approach can encode hardware details, such as finite degrees of reliability, so we also use DECAF to examine implications for approximate hardware design. We find that multi-level architectures can offer advantages over simpler two-level machines and that solver-aided optimization improves efficiency.Keywords
Funding Information
- NSF (1216611)
This publication has 26 references indexed in Scilit:
- Expressing and verifying probabilistic assertionsPublished by Association for Computing Machinery (ACM) ,2014
- Stochastic optimization of floating-point programs with tunable precisionACM SIGPLAN Notices, 2014
- Expressing and verifying probabilistic assertionsACM SIGPLAN Notices, 2014
- Quality programmable vector processors for approximate computingPublished by Association for Computing Machinery (ACM) ,2013
- Verifying quantitative reliability for programs that execute on unreliable hardwarePublished by Association for Computing Machinery (ACM) ,2013
- Energy typesPublished by Association for Computing Machinery (ACM) ,2012
- Architecture support for disciplined approximate programmingPublished by Association for Computing Machinery (ACM) ,2012
- Z3: An Efficient SMT SolverLecture Notes in Computer Science, 2008
- Interlanguage migrationPublished by Association for Computing Machinery (ACM) ,2006
- A methodology for procedure cloningComputer Languages, 1993