Tadashi: Enabling AI-Based Automated Code Generation With Guaranteed Correctness

TL;DR

Tadashi is a system that combines the polyhedral model with machine learning to generate code transformations that are guaranteed to be correct and legal, addressing the reliability issues of black-box ML approaches.

Contribution

It introduces Tadashi, a novel end-to-end framework that guarantees correctness of ML-generated code transformations using formal methods and supports dataset curation for ML models.

Findings

Guarantees legality of generated transformations.

Demonstrates low runtime overhead.

Shows broad applicability across code transformations.

Abstract

Frameworks and domain-specific languages for auto-generating code have traditionally depended on human experts to implement rigorous methods ensuring the legality of code transformations. Recently, machine learning (ML) has gained traction for generating code optimized for specific hardware targets. However, ML approaches-particularly black-box neural networks-offer no guarantees on the correctness or legality of the transformations they produce. To address this gap, we introduce Tadashi, an end-to-end system that leverages the polyhedral model to support researchers in curating datasets critical for ML-based code generation. Tadashi provides an end-to-end system capable of applying, verifying, and evaluating candidate transformations on polyhedral schedules with both reliability and practicality. We formally prove that Tadashi guarantees the legality of generated transformations, demonstrate its low runtime overhead, and showcase its broad applicability. Tadashi available at https://github.com/vatai/tadashi/.