测试消息传递并发性的复杂性

《Proceedings of the ACM on Programming Languages》：The Complexity of Testing Message-Passing Concurrency

本研究探讨基于通道的并发程序一致性验证问题，提出考虑多线程数、通道数及容量等参数的算法，通过多项式上界和困难性下界分析复杂度，并验证其百万级事件处理性能优于约束求解方法。

　　

摘要AI摘要

要查看此由AI生成的摘要，您必须拥有高级访问权限。

了解更多登录

摘要

摘要

在并发程序的自动化测试和验证中，一个关键的计算问题是一致性问题——给定部分执行历史，是否可以以一致的方式完成剩余的执行？由于其重要性，一致性测试已被广泛研究，应用于内存模型以及数据库隔离级别。在所有这些场景中，一个共同的特点是使用共享内存作为线程间通信的主要方式。另一方面，现代编程语言（如Go、Rust和Kotlin）提倡转向基于通道（即消息传递）的通信范式。然而，基于通道的并发的一致性问题目前尚不甚明了。

在本文中，我们将对基本一致性问题的研究扩展到通道领域，考虑了各种输入参数，例如执行的线程数量、通道数量和通道容量。我们绘制了一个复杂的复杂性图谱，包括在某些输入参数固定时的多项式上界，以及难度下界。我们的上界基于可以在自动化验证工具中驱动通道一致性验证的算法。我们的下界指出了足以引发难度问题的最小输入参数，从而揭示了测试基于通道的并发性的复杂性。结合这些上界和下界，我们描述了验证通道一致性可解性/不可解性的边界，并表明我们的算法通常是（几乎）最优的。我们还实现了主要的一致性检查算法，并设计了优化措施以提高其性能。我们使用从开源Go项目中获得的103个实例评估了该实现的性能，并将其与基于约束解决的算法进行了比较。实验结果表明，我们的一致性检查算法非常强大；它可以处理大约100万个事件，并且在运行时间性能上显著优于基于约束解决的方法。

AI摘要

要查看此由AI生成的纯文本摘要，您必须拥有高级访问权限。