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.