使用确定性线程调度程序的并行基于属性的测试

这是一篇关于如何以可重现的方式编写测试以捕获竞态条件的文章,主要内容如下:

  • 背景:在之前的文章中介绍了从顺序假代码机械派生并行测试以发现竞态条件的方法,该方法是黑盒测试技术,但线程交错不同会导致测试结果不同,影响失败测试用例的缩减。作为解决方法,建议在未修改的代码中发现竞态条件时,将共享内存模块替换为在操作周围引入睡眠的模块,以减少不确定性并帮助缩减。本文将实现确定性调度程序,以实现每次运行多线程程序时都能获得相同的线程交错。
  • 动机和概述:以两个线程同时递增计数器的竞态条件为例,说明大多数编程语言中线程交错是不确定的,导致不可重现的失败。提出通过在每个共享内存操作周围插入暂停,并让调度程序一次取消暂停一个线程的想法,以实现确定性调度。本文将把 matklad 的确定性调度程序从 Rust 移植到 Haskell,并将其与并行属性测试机制挂钩。
  • 确定性调度程序:可分为三部分实现。一是实现生成的线程与调度程序的通信方式,使用 Haskell 的TMVar进行通信;二是创建围绕 Haskell 线程的包装数据类型ManagedThreadId;三是实现确定性调度程序本身,等待所有线程暂停,然后逐步执行一个线程,直到它暂停或完成。
  • 并行属性测试回顾:对于更复杂的并发场景,需要基于顺序模型的正确性标准,如 Herlihy 和 Wing 的线性化,以隐藏不确定性和崩溃线程的复杂性,并在任意数据结构上工作。
  • 将调度程序集成到测试中:需要在三个地方更改之前的代码,包括顺序模块、并行模块和计数器示例。在顺序模块中,将runCommandMonad方法移动到StateModel类中,并使用单线程Signal;在并行模块中,重新使用 QuickCheck 的种子,并使用确定性调度程序修改runParallelCommands函数;在计数器示例中,用共享内存接口操作替换睡眠和直接共享内存操作,并传递Signal通信通道。
  • 结论和进一步工作:介绍了确定性测试多线程代码的方法及其在并行属性测试中的应用,指出可以在几个方面进行改进,如改善收缩以获得最小反例、枚举所有交错、将白盒方法转换为黑盒方法、考虑其他一致性模型、部分顺序减少以及测试其他并发数据结构等。欢迎反馈和合作。
  • 致谢:感谢 Daniel Gustafsson 讨论解决收缩导致不同线程交错的问题。

文中还详细介绍了相关代码实现和示例,如确定性调度程序的各个部分代码、计数器示例的修改等。

阅读 9
0 条评论