Probability Type Inference for Flexible Approximate Programming

In approximate computing, programs gain efficiency by al-lowing occasional errors. Controlling the probabilistic ef-fects 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 de-gree of approximation. A combination of type inference, code specialization, and optional dynamic tracking makes the system expressive and convenient. The core type sys-tem captures the probability that each operation exhibits an error and bounds the probability that each expression devi-ates from its correct value. Solver-aided type inference lets the programmer specify the correctness probability on only some variables—program outputs, for example—and auto-matically 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 annota-tion burden. Our constraint-based approach can encode hard-ware details, such as finite degrees of reliability, so we also use DECAF to examine implications for approximate hard-ware design. We find that multi-level architectures can offer advantages over simpler two-level machines and that solver-aided optimization improves efficiency. Categories and Subject Descriptors D.3.3 [Programmin