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.
I haven't had a chance to look at bbqueue, but I recall (wow, I guess more than two years ago) difficulty designing patterns to use DMA due to aliasing concerns over the buffers given to DMA peripherals. What's the state of the art for that today? Did you folks ever find a nice abstraction?
This post also reminds me to check up on embedded async executors. Using interrupts to drive native async code is still a dream that keeps me up at night with excitement.
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.
Also the title in the article uses "SPARK", while on HN it's "Spark". Those are different spellings, with different characters. It's not safe to assume case can be changed without altering meaning in general.
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.
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