Fast and Efficient Bit-Level Precision Tuning
Par Dorra Ben Khalifa Dorra (LAMPS, UPVD) le 2021-11-26*
- Although users of High Performance Computing (HPC) are most interested in raw performance, both storage costs and power consumption have become critical concerns. This is due to several technological issues such as the power limitation of processors and the massive cost of communications which arise when executing applications on such architectures. In recent years, the use of precision tuning to improve the performance metrics is emerging as a new trend to save the resources on the available processors. In this thesis, we introduce a new technique for precision tuning radically different from the existing ones.
The main idea of our approach is based on a semantic modelling of the propagation of the numerical errors throughout the program source. This yields a system of constraints whose minimal solution gives the best tuning of the program. Based on a static analysis approach, we formulate the problem of precision tuning with two different methods. The first method combines a forward and a backward error analysis which are two popular paradigms of error analysis. Next, our analysis is expressed as a set of linear constraints, made of propositional logic formulas and relations between integer elements only, checked by a SMT solver. The second method consists of generating an Integer Linear Problem (ILP) from the program. 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 bit-level. A finer set of semantic equations is also proposed which does not reduce directly to an ILP problem. So, we use the policy iteration technique to find a solution. Both methods have been implemented in a tool named, POP. We provide in this thesis a detailed evaluation of the performance of POP on several benchmarks coming from various application domains such as embedded systems, Internet of Things (IoT), physics, etc. Also, we show that our results of precision tuning encompass the results of the state-of-the-art tools in several manners.
Keywords: Computer arithmetic, numerical accuracy, static analysis, constraint generation, SMT solver, LP solver, policy iteration.