}
/* Here once_control->inited > 0. */
if (InterlockedDecrement (&once_control->num_threads) == 0)
- /* once_control->num_threads is now zero, and once_control->inited is 1.
+ /* once_control->num_threads is now zero, and once_control->inited > 0.
No other thread will need to use the lock.
We can therefore destroy the lock, to free resources. */
- DeleteCriticalSection (&once_control->lock);
+ /* If once_control->inited is == 1, set it to 2. */
+ if (InterlockedCompareExchange (&once_control->inited, 2, 1) == 1)
+ DeleteCriticalSection (&once_control->lock);
}
+ /* Proof of correctness:
+ * num_threads is incremented and then decremented by some threads.
+ Therefore, num_threads always stays >= 0, and is == 0 at the end.
+ * The first thread to go through the once_control->started fence
+ initializes the lock and moves inited from <= 0 to > 0. The other
+ threads don't move inited from <= 0 to > 0.
+ * inited, once > 0, stays > 0 (since at the place where it is assigned 0,
+ it cannot be > 0).
+ * inited does not change any more once it is 2.
+ Therefore, it can be changed from 1 to 2 only once.
+ * DeleteCriticalSection gets invoked right after inited has been changed
+ from 1 to 2. Therefore, DeleteCriticalSection gets invoked only once.
+ * After a moment where num_threads was 0 and inited was > 0, no thread can
+ reach an InitializeCriticalSection or EnterCriticalSection invocation.
+ Proof:
+ - At such a moment, no thread is in the code range between
+ InterlockedIncrement (&once_control->num_threads)
+ and
+ InterlockedDecrement (&once_control->num_threads)
+ - After such a moment, some thread can increment num_threads, but from
+ there they cannot reach the InitializeCriticalSection invocation,
+ because the once_control->started test prevents that, and they cannot
+ reach the EnterCriticalSection invocation in the other branch because
+ the
+ if (once_control->inited <= 0)
+ test prevents that.
+ * From this it follows that:
+ - DeleteCriticalSection cannot be executed while the lock is taken
+ (because DeleteCriticalSection is only executed after a moment where
+ num_threads was 0 and inited was > 0).
+ - Once DeleteCriticalSection has been executed, the lock is not used any
+ more.
+ */
}