Fast and efficient bit-level precision tuning. (English) Zbl 1497.68105
Drăgoi, Cezara (ed.) et al., Static analysis. 28th international symposium, SAS 2021, Chicago, IL, USA, October 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12913, 1-24 (2021).
Summary: 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.
For the entire collection see [Zbl 1489.68011].
For the entire collection see [Zbl 1489.68011].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 65Y04 | Numerical algorithms for computer arithmetic, etc. |
Keywords:
static analysis; computer arithmetic; integer linear problems; numerical accuracy; policy iterationReferences:
| [1] | ANSI/IEEE: IEEE Standard for Binary Floating-point Arithmetic, std 754-2008 edn. (2008) |
| [2] | Ben Khalifa, D., Martel, M.: Precision tuning and internet of things. In: International Conference on Internet of Things, Embedded Systems and Communications, IINTEC 2019, pp. 80-85. IEEE (2019) |
| [3] | Ben Khalifa, D., Martel, M.: Precision tuning of an accelerometer-based pedometer algorithm for IoT devices. In: International Conference on Internet of Things and Intelligence System, IOTAIS 2020, pp. 113-119. IEEE (2020) |
| [4] | Ben Khalifa, D., Martel, M.: An evaluation of POP performance for tuning numerical programs in floating-point arithmetic. In: 4th International Conference on Information and Computer Technologies, ICICT 2021, Kahului, HI, USA, 11-14 March 2021, pp. 69-78. IEEE (2021) |
| [5] | Ben Khalifa, D.; Martel, M.; Gervasi, O., A study of the floating-point tuning behaviour on the n-body problem, ICCSA 2021 (2021), Cham: Springer, Cham · doi:10.1007/978-3-030-86976-2_12 |
| [6] | Ben Khalifa, D.; Martel, M.; Adjé, A.; Hasan, O.; Mallet, F., POP: a tuning assistant for mixed-precision floating-point computations, Formal Techniques for Safety-Critical Systems, 77-94 (2020), Cham: Springer, Cham · doi:10.1007/978-3-030-46902-3_5 |
| [7] | Cherubin, S.; Agosta, G., Tools for reduced precision computation: a survey, ACM Comput. Surv., 53, 2, 1-35 (2020) · doi:10.1145/3381039 |
| [8] | Chiang, W., Baranowski, M., Briggs, I., Solovyev, A., Gopalakrishnan, G., Rakamaric, Z.: Rigorous floating-point mixed-precision tuning. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL, pp. 300-315. ACM (2017) · Zbl 1380.68116 |
| [9] | Costan, A.; Gaubert, S.; Goubault, E.; Martel, M.; Putot, S.; Etessami, K.; Rajamani, SK, A policy iteration algorithm for computing fixed points in static analysis of programs, Computer Aided Verification, 462-475 (2005), Heidelberg: Springer, Heidelberg · Zbl 1081.68616 · doi:10.1007/11513988_46 |
| [10] | Cousot, P.; Sagiv, M., The ASTREÉ analyzer, Programming Languages and Systems, 21-30 (2005), Heidelberg: Springer, Heidelberg · Zbl 1108.68422 · doi:10.1007/978-3-540-31987-0_3 |
| [11] | Darulova, E., Horn, E., Sharma, S.: Sound mixed-precision optimization with rewriting. In: Proceedings of the 9th ACM/IEEE International Conference on Cyber-Physical Systems, ICCPS, pp. 208-219. IEEE Computer Society/ACM (2018) |
| [12] | Diffenderfer, J.; Fox, A.; Hittinger, JAF; Sanders, G.; Lindstrom, PG, Error analysis of ZFP compression for floating-point data, SIAM J. Sci. Comput., 41, 3, A1867-A1898 (2019) · Zbl 07099317 · doi:10.1137/18M1168832 |
| [13] | Fousse, L., Hanrot, G., Lefèvre, V., Pélissier, P., Zimmermann, P.: MPFR: a multiple-precision binary floating-point library with correct rounding. ACM Trans. Math. Softw. 33, 13-es (2007) · Zbl 1365.65302 |
| [14] | Guo, H., Rubio-González, C.: Exploiting community structure for floating-point precision tuning. In: Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2018, pp. 333-343. ACM (2018) |
| [15] | Gustafson, Y.: Beating floating point at its own game: posit arithmetic. Supercomput. Front. Innov. Int. J. 4(2), 71-86 (2017). doi:10.14529/jsfi170206 |
| [16] | Kotipalli, P.V., Singh, R., Wood, P., Laguna, I., Bagchi, S.: AMPT-GA: automatic mixed precision floating point tuning for GPU applications. In: Proceedings of the ACM International Conference on Supercomputing, ICS, pp. 160-170. ACM (2019) |
| [17] | Lam, M.O., Hollingsworth, J.K., de Supinski, B.R., LeGendre, M.P.: Automatically adapting programs for mixed-precision floating-point computation. In: International Conference on Supercomputing, ICS 2013, pp. 369-378. ACM (2013) |
| [18] | Martel, M.; Barrett, C.; Davies, M.; Kahsai, T., Floating-point format inference in mixed-precision, NASA Formal Methods, 230-246 (2017), Cham: Springer, Cham · doi:10.1007/978-3-319-57288-8_16 |
| [19] | McKeeman, WM, Algorithm 145: adaptive numerical integration by Simpson’s rule, Commun. ACM, 5, 12, 604 (1962) |
| [20] | Morris, D., Saponas, T., Guillory, A., Kelner, I.: RecoFit: using a wearable sensor to find, recognize, and count repetitive exercises. In: Conference on Human Factors in Computing Systems (2014) |
| [21] | de Moura, L.; Bjørner, N.; Ramakrishnan, CR; Rehof, J., Z3: an efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 337-340 (2008), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-78800-3_24 |
| [22] | Papadimitriou, CH, On the complexity of integer programming, J. ACM (JACM), 28, 4, 765-768 (1981) · Zbl 0468.68050 · doi:10.1145/322276.322287 |
| [23] | Parker, D.S.: Monte Carlo arithmetic: exploiting randomness in floating-point arithmetic. Technical report CSD-970002, University of California (Los Angeles) (1997) |
| [24] | Rubio-González, C., et al.: Precimonious: tuning assistant for floating-point precision. In: International Conference for High Performance Computing, Networking, Storage and Analysis, SC 2013, pp. 27:1-27:12. ACM (2013) |
| [25] | Schrijver, A., Theory of Linear and Integer Programming (1998), New York: Wiley, New York · Zbl 0970.90052 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
