A Systematic Translation Validation Framework for Mlir-Based Compilers

Published In

International Journal of Software Engineering and Knowledge Engineering

Document Type

Citation

Publication Date

7-19-2024

Abstract

This paper introduces an innovative translation validation framework designed for MLIR-based compilers, which has garnered considerable prominence in fields such as machine learning, high-performance computing and hardware design. Despite rigorous testing, compilers based on MLIR might still induce incorrect results and undefined behaviors, necessitating verification work. Our framework first takes a pair of MLIR programs as inputs and check their function signature’s compatibility before encoding them into SMT expressions. Then it uses the Z3 SMT solver to check whether the target program refines the source program. Our framework transcends the dialect limitations of past solutions, thereby providing validation support to a wider range of MLIR-based compilers. We demonstrate its effectiveness through evaluations on prominent open-source MLIR-based compilers, where we identified bugs and undefined behaviors. We further demonstrate the capability of this framework by validating two practical deep-learning accelerator designs.

Rights

© 2024 World Scientific Publishing Co Pte Ltd

DOI

10.1142/S021819402450030X

Persistent Identifier

https://archives.pdx.edu/ds/psu/42517

Share

COinS