Presentation

· Contributors · Organizations · Search Program · My Schedule

Formal Approaches to Characterize Emerging Arithmetic Realizations

SessionResearch, ACM SRC, and Doctoral Showcase Posters

DescriptionAs HPC models grow increasingly complex, disparities in floating point implementations across hardware platforms begin to pose significant challenges to reproducibility and reliability. This is especially so, given that HPC employs hardware optimized for performance, which quite often deviates from the IEEE Standard. We leverage SMT solvers, particularly Z3, to develop a rigorous framework for analyzing and verifying the behavior of computer arithmetic implementations in emerging hardware realizations. Using bit-vectors to model IEEE non-standard behaviors, we are able to formally reason about intricate deviations in areas such as rounding rules, subnormal number handling, precision, normalization, etc. We demonstrate the framework's utility in two key applications: automating feature-targeted hardware testing for undocumented features and uncovering the degree of conformance to deeper properties such as monotonicity within these non-standard arithmetics. Our work also directly benefits cutting-edge GPU implementations, which is a timely issue underlying trust in scientific computation.

Authors

Paul Jiang

Purdue University

Iana Lin

University of California, Berkeley