It is critical that compilers are correct! Finding bugs is one aspect of testing the correctness of compilers in wide use today. A compiler is correct if every compiled program behaves as allowed by the semantics of its source code - else there is a bug. Memory consistency models define the semantics of concurrent programs. We focus on how to detect concurrency bugs introduced by compilers, as identified using memory models. We seek a testing technique that automatically covers concurrency bugs up to fixed bounds on program sizes and that scales to find bugs in compiled programs with many lines of code. Otherwise, a testing technique can miss bugs. Unfortunately, the state-of-the-art techniques are yet to satisfy all of these properties. We present the T\'el\'echat compiler testing tool for concurrent programs. T\'el\'echat finds a concurrency bug when the behaviour of a compiled program, as allowed by its architecture memory model, is not a behaviour of the source program under its source model. We make three claims: T\'el\'echat improves the state-of-the-art at finding bugs in code generation for multi-threaded execution, it is the first public description of a compiler testing tool for concurrency that is deployed in industry, and it is the first tool that takes a significant step towards the desired properties. We provide experimental evidence suggesting T\'el\'echat finds bugs missed by other state-of-the-art techniques, case studies indicating that T\'el\'echat satisfies the properties, and reports of our experience deploying T\'el\'echat in industry.
翻译:编译器的正确性至关重要!发现缺陷是测试当前广泛使用编译器的正确性的重要方面。若每个编译后程序的行为均遵循其源代码语义所允许的范围,则编译器正确——反之则存在缺陷。内存一致性模型定义了并发程序的语义。本文聚焦于如何检测由编译器引入的并发缺陷(通过内存模型识别)。我们寻求一种测试技术,该技术能自动覆盖程序规模有界范围内的并发缺陷,并可扩展至发现数千行代码的编译后程序中的缺陷——否则测试技术可能遗漏缺陷。然而,现有最先进技术尚未完全满足这些特性。我们提出面向并发程序的Télécahat编译器测试工具。当编译后程序的行为(由其架构内存模型所允许)不属于源程序在其源模型下的行为时,Télécahat即发现并发缺陷。我们提出三项主张:Télécahat提升了多线程执行代码生成缺陷检测的现有技术水平;这是业界首次公开描述已部署使用的并发编译器测试工具;该工具是首个向理想特性迈出重大步伐的测试工具。我们通过实验证据表明Télécahat能发现被其他现有最优技术遗漏的缺陷,通过案例研究证实其满足相关特性,并分享在业界部署Télécahat的应用经验。