Research Projects

Compiler optimization is a crucial stage that benefits by improving the runtime of the software. Still, none of the compiler optimizations is guaranteed to optimize (i.e., runtime improvement) all the programs in every scenario. These optimizations are very sensitive to the code structure of the programs and the architecture details. There has always been consistent improvement over the hardware specification, and to match that specification, compiler engineers tend to do manual performance analysis to find the regression or possible improvements. Profiling-based techniques are commonly used to identify performance bottlenecks. These techniques involve running benchmarks, collecting logs, and then performing mostly manual analysis to identify issues and recommend optimizations to developers. However, this approach has two primary limitations. First, obtaining logs can be challenging due to large file sizes or restrictions from customers. Second, manual log analysis is time-consuming, repetitive, and prone to errors. Machine learning-based approaches are being explored to achieve similar objectives, but their effectiveness is limited by a lack of comprehensive training datasets containing both unoptimized and optimized codebases. Consequently, ML-based techniques have yet to mature for this application. Formal methods, a branch of computer science, verify specific system properties using mathematical reasoning. However, scalability remains a major challenge with this technique, discouraging many compiler experts from integrating SMT solvers directly into the compilation process. Nevertheless, these solvers can be applied outside the main compilation pipeline to achieve similar verification goals while enabling additional lightweight optimizations. Given the advantages and limitations of previous methods, there is a clear need for a formal-method-based automated tool to address this challenge. The proposed tool would take the target software and system specifications as input, analyzing them to identify potential optimization opportunities aligned with the given specifications. This project aims to develop a performance optimization tool grounded in formal methods, utilizing the LLVM compiler infrastructure. The project focuses on two primary objectives: first, to design a tool that analyzes software inputs to identify optimization opportunities through formal software analysis; second, to address this optimization gap with a lightweight compiler pass that applies targeted transformations to achieve performance gains. The outcomes of this project will be relevant for research communities in compilers, formal methods, programming languages, and software engineering. Beyond academic contributions, the project holds practical value, offering automated performance analysis capabilities that can enhance software efficiency across industries.