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.