From Rust to Spark: Formally Proven Bip-Buffers

Hey! James from Ferrous here. I'm super excited to see the work Fabien has done here wrt the bbqueue algorithm, and pretty excited to see Rust + Ada/Spark working together to build more reliable libraries and tools for both ecosystems :).

I definitely want to give credit to Andrea Lattuada [1] from the Systems group at ETH Zurich, who I worked with to design the algorithm behind bbqueue, as well as Simon Cooke [2], the original author of the bip-buffer algorithm we based bbqueue on (with some thread-safe changes).

Happy to answer any questions (though my knowledge of Ada/Spark is limited), especially on the algorithm or the Rust implementation. I use it super often for embedded systems, and it also allows for ridiculous performance even on PC/Desktop/Server systems.

[1]: https://twitter.com/utaal [2]: https://twitter.com/FleetingShadow

As you might infer from the domain (ADA core), this is about SPARK the a formally defined computer programming language based on the Ada programming language, intended for the development of high integrity software used in systems where predictable and highly reliable operation is essential.

This is not about Spark, the data processing system written in Scala.

Interesting variation on circular queue. It looks like it is mostly useful when the size of the data chunk varies, but the consumer never reads across the boundry of a chunk. Something like variable length packets/messages would be a good fit. If the data chunk size was fixed, you could just size you circular queue to be a multiple of that. And I can't think of anyway to ensure contiguous memory if the consumers' read sizes are not aligned with the producer's write sizes something I encounter frequently with streaming data architectures (like gnuradio for example) where the ideal chunk size varies between the different algorithms in different processing nodes in the pipeline.