SRWLock seems like a situation where it's small enough for you to construct proofs that what you did is correct, and important enough that the enormous expense of such proof is justified.
The C++ std::mutex provided in Microsoft's STL is ludicrously big, whereas SRWLocks are the same size as a pointer. In one sense being ludicrously big is great - less risk the std::mutex will mistakenly share a cache line with your unrelated data, but for most people this makes std::mutex annoyingly expensive.
Maybe my memory is faulty but I believe it was analyzed by Leslie Lamports stuff. Ofcourse your building a model of how it should work and you might have faults in that.
C++ std::mutex provided in Microsoft's STL uses SRWLocks underneath, same size as a pointer.
Sadly, SRWLocks have yet another bug, they are very unfair. Write a loop which locks std::mutex inside the body, and no other thread will be able to grab the mutex despite the loop repeatedly releases then re-acquires the mutex. Critical sections are way more fair.
Some time ago I did some test, 256 threads competing on a small number of cache lines, and found out that all, CreateMutex, CRITICAL_SECTION and SRWLOCK, were quite fair.
The most successful thread was only 25%, 15% and 9% ahead of the least successful one.
On the contrary, in my simple usermode spinlock the unfairness would be 1000% or even 2000%.
The C++ std::mutex provided in Microsoft's STL is ludicrously big, whereas SRWLocks are the same size as a pointer. In one sense being ludicrously big is great - less risk the std::mutex will mistakenly share a cache line with your unrelated data, but for most people this makes std::mutex annoyingly expensive.