CCF: Medium: Validating Program Transformations in a Mechanized LLVM

因为我们的计算基础设施的安全性、可靠性和性能取决于其软件的质量，所以提高软件质量对于继续由计算机实现的技术和社会进步至关重要。编译器是构建软件时使用的主要工具，因此是至关重要的——如果开发人员要创建新的、可用的、没有导致崩溃和易受恶意软件攻击的缺陷的软件，编译器的正确性是必不可少的。这个项目的目标是提供一种方法来验证现代计算平台的编译器转换的正确性，强调设计用于多核体系结构的软件。本研究探讨了为LLVM（低级虚拟机）基础设施构建程序转换验证器的技术，LLVM是一种用于工业编译器的开源中间语言。研究人员将定义LLVM程序符号求值的指义语义，并证明（在交互定理证明器Coq中）符号求值结果的解释与操作语义一致。为了考虑多核、共享内存的计算机体系结构，该项目将定义一个并发内存模型，通过目标体系结构配置参数化，从而保证无数据竞争程序的顺序一致性。该模型的语义将具有足够的表达能力来表示程序行为，并且适合于机械化证明。如果成功，这项研究将降低开发和测试编译器的成本，并提高我们对编程语言实现的理解，特别是在多核处理器上，从而导致一个更可靠、更安全、更经济的计算生态系统。

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.