mirror of
https://github.com/RGBCube/serenity
synced 2025-07-27 20:47:45 +00:00
LibCore: Introduce SharedSingleProducerCircularQueue
This new class with an admittedly long OOP-y name provides a circular queue in shared memory. The queue is a lock-free synchronous queue implemented with atomics, and its implementation is significantly simplified by only accounting for one producer (and multiple consumers). It is intended to be used as a producer-consumer communication datastructure across processes. The original motivation behind this class is efficient short-period transfer of audio data in userspace. This class includes formal proofs of several correctness properties of the main queue operations `enqueue` and `dequeue`. These proofs are not 100% complete in their existing form as the invariants they depend on are "handwaved". This seems fine to me right now, as any proof is better than no proof :^). Anyways, the proofs should build confidence that the implemented algorithms, which are only roughly based on existing work, operate correctly in even the worst-case concurrency scenarios.
This commit is contained in:
parent
b0a2572577
commit
6b13436ef6
5 changed files with 440 additions and 0 deletions
|
@ -164,6 +164,7 @@ set(SERVICE_DEBUG ON)
|
|||
set(SH_DEBUG ON)
|
||||
set(SHELL_JOB_DEBUG ON)
|
||||
set(SH_LANGUAGE_SERVER_DEBUG ON)
|
||||
set(SHARED_QUEUE_DEBUG ON)
|
||||
set(SIGNAL_DEBUG ON)
|
||||
set(SLAVEPTY_DEBUG ON)
|
||||
set(SMP_DEBUG ON)
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue