An Automated Verification Framework for HalideIR-Based Compiler Transformations

Published In

2023 Design, Automation & Test in Europe Conference & Exhibition

ISBN

979-8-3503-9624-9

Document Type

Citation

Publication Date

4-2023

Subjects

Deep learning (Machine learning), Compilers (Computer programs), Electronic systems -- Design and construction

Abstract

HalideIR is a popular intermediate representation for compilers in domains such as deep learning, image processing, and hardware design. In this paper, we present an automated verification framework for HalideIR-based compiler transformations. The framework conducts verification using symbolic execution in two steps. Given a compiler transformation, our automated verification framework first uses symbolic execution to enumerate the compiler transformation's paths, and then utilizes symbolic execution to verify if the output program for each transformation path is equivalent to its source. We have successfully applied this framework to verify 46 transformations from the three most-starred HalideIR-based compilers on GitHub and detected 4 transformation bugs undetected by manually crafted unit tests.

Keywords: Deep learning; Program processors; Image processing; Computer bugs; Hardware; Software development management

Rights

Copyright © 2023 by the Institute of Electrical and Electronics Engineers, Inc.
All rights reserved.

Locate the Document

PSU Affiliates:
Access the Online Version via Library Subscription

Non-affiliates can access via their library or the publisher:
https://doi.org/10.23919/DATE56975.2023.10137308

DOI

10.23919/DATE56975.2023.10137308

Persistent Identifier

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

Share

COinS