同步反转数据竞争的乐观预测

动态数据竞争检测已成为实践中确保并发软件可靠性的关键技术。然而，由于线程调度器的非确定性，动态方法常常会遗漏数据竞争。预测性竞争检测技术通过推断可能暴露数据竞争的替代执行而不重新执行底层程序，来弥补这一不足。更形式化地说，动态数据竞争预测问题问的是：给定并发程序执行的一条迹 σ，能否将 σ 正确重排以暴露一个数据竞争？现有的最先进数据竞争预测技术要么无法扩展到真实并发软件产生的执行，要么只能暴露有限类别的数据竞争，例如那些无需反转同步操作顺序即可暴露的竞争。一般来说，通过推理同步反转来暴露数据竞争是一个难解问题。在这项工作中，我们识别出一类称为乐观同步反转竞争的数据竞争，它们可以以易处理的方式被检测到，并且通常包含先前易处理技术无法暴露的非平凡数据竞争。我们还提出了一种可靠的算法 OSR，用于在总体二次时间内检测所有乐观同步反转数据竞争，并通过建立匹配的下界证明该算法是最优的。我们的实验在广泛的基准测试套件上证明了 OSR 的有效性，OSR 报告了最多数量的数据竞争，并能很好地扩展到大型执行迹。