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.
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!