如何正式验证 C++ 中的 WaitGroup 实现的正确性？

Question

描述

我在 C++ 中实现了一个 WaitGroup 假设：

1. 用户必须确保计数器值不会低于零。
2. WaitGroup 可以重复使用。

下面是我的代码：

class WaitGroup {
 public:
  void Add(size_t count) {
    lock_guard<mutex> lock(mutex_);
    count_ += count;
  }

  void Done() {
    lock_guard<mutex> lock(mutex_);
    if (--count_ == 0) {
      cv_.notify_all();
    }
  }

  void Wait() {
    unique_lock<mutex> lock(mutex_);
    cv_.wait(lock, [this] { return count_ == 0; });
  }

 private:
  size_t count_{0};
  mutex mutex_;
  condition_variable cv_;
};

问题

我如何正式验证我的 WaitGroup 实现的正确性？ 证明这些事情的一般方法是什么？

Answer 1

为了正式验证类的正确性，您需要绘制逻辑可能采取的所有可能路径，并从数学上证明它确实做了它应该做的事情。所以，我们可以说这实际上是不可能的（不是以快速和自动化的方式）。

但是我可以告诉您如何增加实现无错误的机会。第一步是定义需求。你的

用户必须确保计数器值不会低于零

声明已经有缺陷，因为这里

count_

是一个私有字段，一个实现细节，你不应该依赖它。更好的要求是：

• 用户可以

  Add

  任意数量的任务
• 用户应有可能

  Wait

  （阻塞）完成所有当前任务（即活动任务数为0）
• 用户可以将单个任务标记为

  Done

• WaitGroup

  应是线程安全的

• WaitGroup

  可重复使用

然后设计测试来满足要求。我想到的第一个明显的场景是：

异步添加 10 个任务到队列中，然后异步将它们全部标记为 DONE，然后等待

TEST(xxx, yyy) {
    WaitGroup sut;
    std::vector<std::future<void>> tasks;
    constexpr int NUM_TASKS = 10;
    for (int i = 0; i < NUM_TASKS; i++) {
        tasks.push_back(std::async(std::launch::async, [&]() {
            sut.Add(1);
        }));
    }
    tasks.clear();  // join all threads to have all tasks added
    for (int i = 0; i < NUM_TASKS; i++) {
        tasks.push_back(std::async(std::launch::async, [&]() {
            sut.Done();
        }));
    }
    sut.Wait();  // what if never returns? problem?
    // then run the above logic once again, to test for "reusable" requirement
}

在此测试中，您可以立即发现一些问题，例如：

• 如果

  sut.Wait()

  由于错误或误用而永远不会返回怎么办？也许你应该添加一个

  int timeout

  参数并在 wait_for 返回

  false

  时抛出异常？
• 如果

  Done

  被调用的次数多于

  Add(1)

  怎么办？当前您有 unsigned int 下溢，也许您应该抛出异常，或者打印警告并使其无操作？
• 还检查用户使用

  Add(x)

   调用 

  x > 1
时的场景
• [优化]确实需要

  std::mutex

  ，也许你可以用

  std::atomic_int

  达到同样的效果？

因此，您可能会稍微改变一下您的接口、实现，并编写更多测试来覆盖不同的极端情况。然后，您可以使用可以检测不同内存和线程错误的工具（例如 valgrind）运行您的套件，并且您将有很好的机会部署高质量的代码。