Modern GPUs feature specialized hardware units that enable high-performance, asynchronous dataflow execution. However, the conventional SIMT programming model is fundamentally misaligned with this task-parallel hardware, creating a significant programmability gap. While hardware-level warp specialization is the key to unlocking peak performance, it forces developers to manually orchestrate complex, low-level communication and software pipelines—a process that is labor-intensive, error-prone, and unsustainable. To address this challenge, we present Tawa, an automated compiler that systematically generates high-performance, warp-specialized code from a high-level, tile-based program. Central to our approach is a novel IR abstraction, asynchronous references (aref), which expresses warp-level communication without exposing low-level hardware details. Using this abstraction, Tawa automatically partitions programs into producer-consumer roles and manages the intricate dataflow pipeline, relieving developers of invasive kernel rewriting. Evaluation on NVIDIA H100 GPUs across representative LLM kernels shows that Tawa delivers high hardware utilization, achieving up to 1.1 × speedup over highly optimized cuBLAS GEMM kernels. For attention workloads, Tawa attains 1.2× speedup over Triton and matches the performance of the hand-optimized CUTLASS C++ FlashAttention-3 kernel with far less programming effort.

Program generation allows us to produce high-performance code specialized to each application domain. Although it has made great success in various domains, it remains to be seen whether it is effective for cryptography where the correctness of programs is indispensable. This work presents a unified approach to program generation, analysis and verification. Our target is Number-Theoretic Transform (NTT), a key building block of several candidates in Post Quantum Cryptography. We develop a program-generation framework based on the typed tagless-final style, and obtained highly efficient implementations with vector instructions such as AVX2 and AVX-512. The framework allows us to implement a program analyzer for integer-overflow analysis. By combining a brute-force analysis with the standard static interval analysis, we have obtained more precise results than the state-of-the-art static analyzer, which let us find a new optimization. We have verified the generated program using the framework. While verifying the generated program all at once is intractable, we can separately verify the low-level components and the high-level algorithm, thanks to the compositional nature of our program generator. We have used an SMT solver for the former and a custom symbolic interpreter for the latter to prove the functional correctness of the generated program successfully.

Automatic optimization for tensor programs becomes increasingly important as we deploy deep learning in various environments, and efficient optimization relies on a rich search space and effective search. Most existing efforts adopt a search space which lacks the ability to efficiently enable domain experts to grow the search space. This paper introduces MetaSchedule, a domain-specific probabilistic programming language abstraction to construct a rich search space of tensor programs. Our abstraction allows domain experts to analyze the program, and easily propose stochastic choices in a modular way to compose program transformation accordingly. We also build an end-to-end learning-driven framework to find an optimized program for a given search space. Experimental results show that MetaSchedule can cover the search space used in the state-of-the-art tensor program optimization frameworks in a modular way. Additionally, it empowers domain experts to conveniently grow the search space and modularly enhance the system, which brings 48% speedup on end-to-end deep learning workloads.