I built this small bounded work queue in C using pthread_mutex_t and pthread_cond_t.

I wrote this because I found many C queue examples online skip the "boring" parts of correctness—like memory visibility and invariant preservation—in favor of performance. I wanted a version where I could prove to myself why it works under heavy contention.

Key Design Choices:

Single-mutex design: Keeps the mental model simple and leverages the "Release-Acquire" semantics guaranteed by pthreads for memory visibility.

Two condition variables: Uses not_full and not_empty with while loops to robustly handle spurious wakeups.

Explicit Invariants: The project documents structural, behavioral, visibility, and liveness invariants.

Verification:

Tested under contention with multiple producers/consumers.

Verified with ASan, UBSan, and TSan (no races or UB detected).

It’s intended as a clear, correct baseline for when the bottleneck is the task processing rather than the lock itself.

Design notes and reasoning: https://emmanuel326.github.io/notes/bounded-queue.html

I'd love to hear feedback on the implementation or the way I've framed the invariants!