Formal verification ensures correct use of machine learning accelerators
Verification of Compiler-to-Accelerator Mappings for Machine Learning Accelerators
Programming Languages
Summary
Machine learning programs often use special hardware to run faster, but making sure the program and hardware work together correctly is hard. The authors created BOLT, a tool that checks whether the parts of a program moved to specialized hardware do exactly the same thing as the original code. BOLT works even with complicated loops and data layouts and does not need extra details from the compiler. This helps prevent mistakes that could happen when using these hardware accelerators.
What this means in practice
- •For hardware accelerator engineers: Verify that compiler-generated mappings correctly implement hardware accelerator operations before deployment.
- •For ml compiler developers: Check the functional correctness of compiler optimizations that offload code to ML accelerators without needing extra compiler annotations.
Authors
Akash Gaonkar, Mike He, Yi Li, Bo-Yuan Huang, Andrew Cheung, Vishal Canumalla, Gus Henry Smith, Zachary Tatlock, Grigory Fedyukovich, Sharad Malik, Aarti Gupta
Abstract
To meet the performance needs of modern machine learning (ML) applications, ML compiler frameworks support compiler-to-accelerator mappings that offload parts of application code to operations in specialized hardware accelerators. However, most of these frameworks do not verify these mappings down to the hardware level, potentially resulting in functional mismatches. In this paper we propose BOLT, the first framework for formally verifying the correctness of compiler-to-accelerator mappings for coarse-grained intrinsics in ML accelerators, with respect to a formal hardware semantics. BOLT does not require additional information from the compiler, and verifies the functional equivalence of the application code and the code for the mapped hardware accelerator intrinsic, including handling of complex loop nests and tensor data layouts in hardware. It effectively utilizes a pattern of *aligning* software loops with the hardware, followed by *relating* corresponding data layouts, to enable verification using well-aligned product programs. To support these steps, we propose two custom templates --- the sync-skeleton and the layout-sketch --- to guide users in aligning loops and specifying data layout relationships, respectively. We have developed a proof-of-concept prototype for BOLT and use it to successfully verify the correctness of several complex mappings for two recent open-source ML accelerators.