Stefan Mada

Languages, Compilers, and more!

Publications

Translation Validation for LLVM’s AArch64 Backend

ARM-TV is a translation validation tool for LLVM’s AArch64 backend. This tool works by taking a function in LLVM IR and processing it in three phases. First, LLVM lowers it to assembly. Second, ARM-TV lifts the assembly back to LLVM IR. Finally, Alive2 verifies that the lifted IR refines the original IR. This paper found 38 miscompilation bugs. My biggest contribution was implementing the semantics for dozens of ARM instructions as SMT constraints.

In preparation

Minotaur: A SIMD-Oriented Synthesizing Superoptimizer

Minotaur is a superoptimizing LLVM pass that uses program synthesis to improve the quality of its code generation, with a specific focus on integer and floating-point SIMD code. On an Intel Cascade Lake processor, Minotaur achieves an average speedup of 7.3% on the GNU Multiple Precision library (GMP)'s benchmark suite, with a maximum speedup of 13%. On SPEC CPU 2017, Minotaur produces an average speedup of 1.5%, with a maximum speedup of 4.5% for 638.imagick. My largest contribution was creating a large C++ testing framework to ensure the correctness of our semantics using a custom just-in-time compiler with support for AVX-512 intrinsics.

Read Publication