I thought this was super interesting; it's great to see a solid writeup.

The consumer-side mutex works pretty well, until you take an interrupt while holding it; then, you need to make sure you're using an unfair mutex, or you'll get a lock convoy.

The non-blocking version isn't hard to write, though. IIRC, for the Windows threadpool, I used https://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.... for the implementation.

I'm really impressed by the concurrency analysis tool; again for the threadpool, we used model-based-testing to write tests for every permutation of API calls, but we never got down to the level of testing thread execution permutations; that's amazingly good to see, and really builds confidence in their implementation.