Because the safety, reliability, and performance of our computing infrastructure rests on the quality of its software, improving software quality is of prime importance for continuing the technological and social advances made possible by computers. Compilers, the primary tools used in constructing software, are therefore crucial--their correctness is essential if developers are to create new, usable software that is free from flaws that lead to crashes and susceptibility to malware. This goal of this project is to provide a methodology for verifying the correctness of compiler transformations for modern computing platforms, emphasizing software designed to work on multicore architectures.
This research investigates techniques for building program transformation validators for the LLVM (Low-Level Virtual Machine) infrastructure, an open-source intermediate language used in industrial compilers. The researchers will define denotational semantics for symbolic evaluation of LLVM programs, and prove (in the interactive theorem prover Coq) that the interpretations of symbolic evaluation results are consistent with operational semantics. To account for multi-core, shared-memory computer architectures, the project will define a concurrent memory model, parameterized by target architecture configurations, which promises sequential consistency for data race free programs. This model's semantics will be expressive enough to represent program behaviors, and suitable for mechanized proofs. If successful, this research will decrease the cost of developing and testing compilers, and improve our understanding of the programming language implementations, particularly on multi-core processors, thereby leading to a more reliable, secure, and cost-effective computing ecosystem.
