Queue or FIFO is one of the most famous data-structure used in several
algorithms. Ke provides some implementations of it in a functional or
imperative way.
It is a little library with a benchmark
(bechamel or core_bench),
a fuzzer and tests.
We provide a functional interface Fke or an imperative interface Rke.
From what we know, Ke.Rke is faster than Queue from the
standard library or the base package. The type of data that it can store
is limited (only supports the types supported by Bigarray.kind)
, but this is enough for a lot of algorithms. The fast
operations are: put some elements faster than a sequence of Queue.push, and
get some elements faster than a sequence of Queue.pop.
We provide extended implementations (Rke.Weighted and Fke.Weighted) with
a limit on the number of elements stored. The purpose is to limit memory
consumption of the queue when we use it in some contexts (like encoder).
Again, as a part of the MirageOS project, Ke does not rely on C stubs,
Obj.magic and so on.
Author: Romain Calascibetta romain.calascibetta@gmail.com
Documentation: https://mirage.github.io/ke/
The functional implementation Fke comes from Okazaki's queue
implementation with GADT to discard impossible cases.
Rke, Rke.Weighted and Fke.Weighted are limited by kind and follow Xen's
implementation of the shared memory ring-buffer. The length of the internal buffer
is always a power of two - that means for a large number of elements
this kind of queue may not fit your requirements.
A fuzzer was made to compare the standard Queue (as an oracle) with Rke and
Fke. We construct a set of actions (push and pop) and ensure (by GADT) to
never pop an empty queue.