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

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

通道一致性验证复杂度研究：提出算法并优化实现，实验显示其效率显著优于传统约束求解方法，可处理百万级事件。

　　

摘要人工智能摘要

要查看此由人工智能生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

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

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

人工智能摘要

人工智能生成的摘要（实验性）

此摘要是使用自动化工具生成的，未由文章作者撰写或审核。它旨在帮助发现、帮助读者评估相关性，并协助来自相关研究领域的读者理解这项工作。它旨在补充作者提供的摘要，后者仍然是文章的主要摘要。完整文章仍然是权威版本。点击此处了解更多。

点击此处对摘要的准确性、清晰度和实用性进行评论。这样做将有助于改进和未来重新生成的版本。

要查看此由人工智能生成的通俗语言摘要，您必须具有高级访问权限。