Description

I’ve implemented a WaitGroup in C++ assuming that:

1. user must ensure that the counter value does not drop below zero.
2. WaitGroup can be reused.

Below is my code:

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_;
};

Question

How can I formally verify the correctness of my WaitGroup implementation?