C语言中的声音静态数据竞争条件验证：这场“竞赛”已经输了吗？

《ACM Transactions on Programming Languages and Systems》：Sound Static Data Race Verification for C: Is the Race Lost?

C程序静态数据竞争自由验证的挑战与代码模式分析 摘要：本文系统性地识别了20种现实世界C程序中阻碍静态数据竞争自由验证的核心代码模式，包括线程本地数据、无锁同步、动态线程计数等，并通过微基准测试验证了现有工具（如Goblint、Deagle）在这些模式上的局限性，指出当前工具在自动化验证真实程序时存在根本性障碍。

　　在现代软件开发中，C语言因其高效性和灵活性而被广泛使用，尤其是在构建关键基础设施的系统时。然而，由于C语言的并发特性，程序中可能会出现数据竞争（data race），这会导致不可预测的行为、性能问题和系统崩溃。因此，确保C程序的可靠性至关重要。数据竞争的静态检测，特别是确保数据竞争自由（data race freedom）的验证，是一个长期存在的挑战。尽管这一领域在过去十年中进行了大量研究，但大多数实际的数据竞争检测工具已经放弃了严格的正确性（soundness）。那么，是否意味着在现实世界的C程序中，实现一种真正的、有保障的数据竞争自由静态验证是不可能的？本文旨在探讨自动化数据竞争自由验证所面临的障碍，并通过分析一组现实世界的程序，提取出一些代表性的编程习惯（idioms），这些习惯是当前工具难以验证的关键障碍。

本文的主要贡献在于，我们识别出了一些现实世界中广泛使用的编程习惯，这些习惯在静态验证工具中表现出了显著的不足。我们进一步将这些习惯转化为微型基准测试（micro-benchmarks），并将其提交给国际软件验证竞赛（SV-COMP）作为评估任务。通过分析这些习惯在当前最先进的静态验证工具上的表现，我们发现尽管有8个习惯可以被某些工具验证，但这些工具在处理这些习惯时仍然存在显著的不正确性（unsoundness）。此外，有五种工具在现实世界的基准测试中未能返回任何结果，而其余两种工具仅能验证2个程序，其余程序则出现崩溃或不确定的结果。这表明，当前最先进的验证工具在处理现实世界的程序时，既存在表面的障碍，也存在根本性的挑战。

为了更好地理解这些障碍，我们首先回顾了静态软件验证的基本概念及其在数据竞争检测中的作用。我们还分析了现有的数据竞争自由验证基准测试，并指出了它们在现实世界程序中所面临的局限性。虽然SV-COMP提供了大量任务，但这些任务往往过于简单，并且没有充分反映现实世界程序的复杂性。我们发现，当前的验证工具在处理现实世界程序时，常常因规模问题而无法完成验证任务，这表明工具的扩展性（scalability）仍是一个主要障碍。此外，我们还发现了一些特定的编程习惯，这些习惯在现实世界程序中出现频率较高，但当前的验证工具却无法正确识别。

为了验证这些编程习惯的普遍性和挑战性，我们进行了详细的分析，并利用Goblint等工具提取了这些习惯的验证挑战。我们还对这些习惯在现实世界程序中的出现频率进行了统计，以确认它们是否构成了一个广泛存在的问题。结果显示，这些编程习惯在现实世界程序中确实较为常见，但当前的验证工具仍然难以处理它们。

本文的另一个重要贡献是，我们提出了一个新的验证基准测试集，并将其提交给SV-COMP，以帮助研究社区更好地评估工具的性能。通过这种方式，我们希望推动静态数据竞争自由验证技术的发展，并促进工具的改进。此外，我们还讨论了当前工具在处理这些编程习惯时所面临的挑战，包括缺乏对某些库函数的支持、资源限制以及对复杂同步机制的处理不足。

总的来说，本文揭示了静态数据竞争自由验证所面临的挑战，并提出了新的基准测试以帮助研究社区进一步探索和改进验证方法。这些挑战不仅包括技术上的困难，还涉及工具设计和实现上的不足。通过识别和分析这些编程习惯，我们希望能够为未来的研究提供有价值的见解，并推动静态数据竞争自由验证技术的发展。