Fast and Efficient Bit-Level Precision Tuning

In this article, we introduce a new technique for precision tuning. This problem consists of finding the least data types for numerical values such that the result of the computation satisfies some accuracy requirement. State of the art techniques for precision tuning use a trial-and-error approach. They change the data types of some variables of the program and evaluate the accuracy of the result. Depending on what is obtained, they change more or less data types and repeat the process. Our technique is radically different. Based on semantic equations, we generate an Integer Linear Problem (ILP) from the program source code. Basically, this is done by reasoning on the most significant bit and the number of significant bits of the values which are integer quantities. The integer solution to this problem, computed in polynomial time by a classical linear programming solver, gives the optimal data types at the bit level. A finer set of semantic equations is also proposed which does not reduce directly to an ILP problem. So we use policy iteration to find the solution. Both techniques have been implemented and we show that our results encompass the results of state-of-the-art tools.

Authors and Affiliations

1. LAMPS Laboratory, University of Perpignan, 52 Av. P. Alduy, Perpignan, France

   Assalé Adjé, Dorra Ben Khalifa & Matthieu Martel

2. Numalis, Cap Omega, Rond-point Benjamin Franklin, Montpellier, France

   Matthieu Martel

Corresponding author

Correspondence to Dorra Ben Khalifa .

Editors and Affiliations

1. Informal Systems, Inria, ENS, DI - Ecole Normale Supérieure, Paris, France

   Cezara Drăgoi

2. Microsoft Corporation, Redmond, WA, USA

   Suvam Mukherjee

3. Nokia Bell Labs, Murray Hill, NJ, USA

   Kedar Namjoshi

A Appendix

We need a lemma on some algebraic operations stable on the set of functions written as the min-max of a finite family of affine functions. The functions are defined on \(\mathbb R^d\).

Lemma 1

The following statements hold:

• The sum of two min-max of a finite family of affine functions is a min-max of a finite family of affine functions.

• The maximum of two min-max of a finite family of affine functions is a min-max of a finite family of affine functions.

Proof

Let g and h be two min-max of a finite family of affine functions and \(f=g+h\). We have \(g=\min _i\max _j g^{ij}\) and \(h=\min _k\max _l h^{kl}\). Let \(x\in \mathbb R^d\). There exist i, k such that \(f(x)\ge \max _j g^{ij}(x)+\max _l h^{kl}(x)=\max _{j,l} g^{ij}(x)+h^{kl}(x)\). We have also, for all i, k, \(f(x)\le \max _j g^{ij}(x)+\max _l h^{kl}(x)=\max _{j,l} g^{ij}(x)+h^{kl}(x)\). We conclude that \(f(x)=\min _{i,k}\max _{j,l} g^{ij}(x)+h^{kl}(x)\) for all x. We use the same argument for the max. \(\Box \)

Proposition 2

The following results hold:

1. 1.

   Let \(\xi \) the constant function equal to 1. The system \(S_\xi ^1\) can be rewritten as \(\{\mathsf {nsb}\in \mathbb N^{Lab}\mid F(\mathsf {nsb})\le (\mathsf {nsb})\}\) where F maps \(\mathbb R^{Lab}\times \mathbb R^{Lab}\) to itself, \(F(\mathbb N^{Lab}\times \mathbb N^{Lab})\subseteq (\mathbb N^{Lab}\times \mathbb N^{Lab})\) and has coordinates which are the maximum of a finite family of affine order-preserving functions.

2. 2.

   Let \(\xi \) the function such that \(\xi (\ell )\) equals the function defined at Fig. 5. The system \(S_\xi \) can be rewritten as \(\{(\mathsf {nsb},\mathsf {nsb_e})\in \mathbb N^{Lab}\times \mathbb N^{Lab}\mid F(\mathsf {nsb},\mathsf {nsb_e})\le (\mathsf {nsb},\mathsf {nsb_e}) \}\) where F maps \(\mathbb R^{Lab}\times \mathbb R^{Lab}\) to itself, \(F(\mathbb N^{Lab}\times \mathbb N^{Lab})\subseteq (\mathbb N^{Lab}\times \mathbb N^{Lab})\) and all its coordinates are the min-max of a finite family of affine functions.

Proof

We only give details about the system \(S_\xi ^1\) (Fig. 4). By induction on the rules. We write \(L=\{\ell \in Lab\mid F_\ell \text { is constructed }\}\). This set is used in the proof to construct F inductively.

For the rule (CONST), there is nothing to do. For the rule (ID), if the label \(\ell '=\rho (x)\in L\) then we define \(F_{\ell '}(\mathsf {nsb})=\max (F_{\ell '}(\mathsf {nsb}),\mathsf {nsb}(\ell ))\). Otherwise \(F_{\ell '}(\mathsf {nsb})=\mathsf {nsb}(\ell )\). As \(\mathsf {nsb}\mapsto \mathsf {nsb}(\ell )\) is order-preserving and the maximum of one affine function, \(F_{\ell '}\) is the maximum of a finite family of order-preserving affine functions since \(\max \) preserves order-preservation.

For the rules (Add), (Sub), (Mult), (Div), (Math) and (Assign), by induction, it suffices to focus on the new set of inequalities. If \(\ell _1\in L\), we define \(F_{\ell _1}\) as the max with old definition and \(RHS(\mathsf {nsb})\) i.e. \(F_{\ell _1}(\mathsf {nsb})=\max (RHS(\mathsf {nsb}),F_{\ell _1}(\mathsf {nsb}))\) where \(RHS(\mathsf {nsb})\) is the right-hand side part of the new inequality. If \(\ell _1\notin L\), we define \(F_{\ell _1}(\mathsf {nsb})=RHS(\mathsf {nsb})\). In the latter rules, \(RHS(\mathsf {nsb})\) are order-preserving affine functions. It follows that \(F_{\ell _1}\) is the maximum of a finite family of order-preserving affine functions.

The result follows by induction for the rule (SEQ).

The rules (Cond) and (While) are treated as the rules (Add), (Sub), (Mult), (Div), (Math) and (Assign), by induction and the consideration of the new set of inequalities.

The last rule (Req) constructs \(F_{\rho (x)}\) either as the constant function equal to p at label \(\rho (x)\) or the maximum of the old definition of \(F_{\rho (x)}\) and p if \(\rho (x)\in L\). The proof for the system \(S_\xi \) uses the same arguments and Lemma 1. \(\Box \)

Proposition 3 (Algorithm correctness)

The sequence \((\sum _{\ell \in Lab} \mathsf {nsb}^k(\ell ))_{0\le k\le K}\) generated by Algorithm 1 satisfies the following properties:

1. 1.

   \(K<+\infty \) i.e. the sequence is of finite length;

2. 2.

   each term of the sequence furnishes a feasible solution for Problem (11);

3. 3.

   \(\sum _{\ell \in Lab} \mathsf {nsb}^{k+1}(\ell )<\sum _{\ell \in Lab} \mathsf {nsb}^k(\ell )\) if \(k<K-1\) and \(\sum _{\ell \in Lab} \mathsf {nsb}^{K}(\ell )=\sum _{\ell \in Lab} \mathsf {nsb}^{K-1}(\ell )\);

4. 4.

   the number k is smaller than the number of policies.

Proof

Let \(\sum _{\ell \in Lab} \mathsf {nsb}^k(\ell )\) be a term of the sequence and \((\mathsf {nsb}^k,\mathsf {nsb_e}^k)\) be the optimal solution of \(\text {Min}\{\sum _{\ell \in Lab} \mathsf {nsb}(\ell )\mid f^{\pi ^k}(\mathsf {nsb},\mathsf {nsb_e})\le (\mathsf {nsb},\mathsf {nsb_e}),\ \mathsf {nsb}\in \mathbb N^{Lab},\ \mathsf {nsb_e}\in \mathbb N^{Lab}\}\). Then \(F(\mathsf {nsb}^k,\mathsf {nsb_e}^k)\le f^{\pi ^k}(\mathsf {nsb}^k,\mathsf {nsb_e}^k)\) by definition of F. Moreover, \(F(\mathsf {nsb}^k,\mathsf {nsb_e}^k)=f^{\pi ^{k+1}}(\mathsf {nsb}^k,\mathsf {nsb_e}^k)\) and \(f^{\pi ^k}(\mathsf {nsb}^k,\mathsf {nsb_e}^k)\le (\mathsf {nsb}^k,\mathsf {nsb_e}^k)\). This proves the second statement. Furthermore, it follows that \(f^{\pi ^{k+1}}(\mathsf {nsb}^k,\mathsf {nsb_e}^k)\le (\mathsf {nsb}^k,\mathsf {nsb_e}^k)\) and \((\mathsf {nsb}^k,\mathsf {nsb_e}^k)\) is feasible for the minimisation problem for which \((\mathsf {nsb}^{k+1},\mathsf {nsb_e}^{k+1})\) is an optimal solution. We conclude that \(\sum _{\ell \in Lab} \mathsf {nsb}^{k+1}(\ell )\le \sum _{\ell \in Lab} \mathsf {nsb}^k(\ell )\) and the Algorithm terminates if the equality holds or continues as the criterion strictly decreases. Finally, from the strict decrease, a policy cannot be selected twice without terminating the algorithm. In conclusion, the number of iterations is smaller than the number of policies.\(\Box \)

Proposition 4

Let \(G:[0,+\infty )^d\mapsto [0,+\infty )^d\) be an order-preserving function such that \(G(\mathbb N^d)\subseteq \mathbb N^d\). Suppose that the set \(\{y\in \mathbb N^d\mid G(y)\le y\}\) is non-empty. Let \(\varphi :\mathbb R^d\mapsto \mathbb R\) a strictly monotone function such that \(\varphi (\mathbb N^d)\subseteq \mathbb N\). Then, the minimization problem below has an unique optimal solution which is integral.

Proof

Let \(L:=\{x\in [0,+\infty )^d\mid G(x)\le x\}\) and \(u=\inf L\). It suffices to prove that \(u\in \mathbb N^d\). Indeed, as \(\varphi \) is strictly monotone then \(\varphi (u)<\varphi (x)\) for all \(x\in [0,+\infty )^d\) s.t. \(G(x)\le x\) and \(x\ne u\). The optimal solution is thus u. If \(u=0\), the result holds. Now suppose that \(0<u\), then \(0\le G(0)\). Let \(M:=\{y\in \mathbb N^d\mid y\le G(y), y\le u\}\). Then \(0\in M\) and we write \(v:=\sup M\). As M is a complete lattice s.t. \(G(M)\subseteq M\), from Tarski’s theorem, v satisfies \(G(v)=v\) and \(v\le u\). Moreover, \(v\in \mathbb N^d\) and \(v\le u\). Again, from Tarski’s theorem, u is the smallest fixpoint of G, it coincides with v. Then \(u\in \mathbb N^d\).\(\Box \)

Reprints and permissions

© 2021 Springer Nature Switzerland AG

Policies and ethics