Collaborative Research: CS2: On-Demand Semantic Analysis via Program Synthesis

Correct compilation is essential to scientific computing, as it provides the bridge from high-level algorithms in source code to computing machinery. LLVM is a critical backbone in this process, powering compilers and infrastructure for languages including Julia, Python, and Fortran. However, the engineering of LLVM has focused on improving general-purpose code, with relatively little attention given to the particular needs of scientific computing. The central question of this project is: Can compiler infrastructure be redesigned so that scientists can express and statically enforce the complex physical and mathematical constraints that define their work? For example, scientists interested in proving positivity for an advection-diffusion-reaction system should be able to do so statically, though the use of tools that lower the burden of proof. The project's novelties are methods to incrementally synthesize domain-specific and program-specific static analyses. The project's impacts are to integrate correct static analyses into a widely-used compiler, thereby enhancing the work of a broad community of scientists. Ultimately, the goal of this research is a compiler development process in which scientists specify what they want and tools generate the how automatically. This research consists of three technical thrusts toward a new, synthesis-based foundation for compiler construction: (1) synthesizing analyses one transformer at a time, through stochastic search and SMT-based verification; (2) creating semantic MLIR dialects for scientific computing domains, namely floating-point numbers and tensors; and (3) developing project-specific techniques to strengthen correctness claims. A key idea is to model traditionally-manual compiler components as compositions of semantic program transformers: small programs that summarize how instructions behave or how they can be replaced without changing observable behavior. These transformers are learned from examples, specifications, or profiling data, using a combination of symbolic reasoning and abstract interpretation. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria. NSF Award ID: 2546822 | Program: 01002627DB NSF RESEARCH & RELATED ACTIVIT | Principal Investigator: Loris DAntoni | Institution: University of California-San Diego, LA JOLLA, CA | Award Amount: $215,035 View on NSF Award Search: https://www.nsf.gov/awardsearch/show-award/?AWD_ID=2546822 View on Research.gov: https://www.research.gov/awardapi-service/v1/awards/2546822.html