News for hackers. Stuff that matters.

A comment on A lock-free ring-buffer with contiguous reservations (2019). Parent comment

Re:A lock-free ring-buffer with contiguous reservations (2019) by jamesmunns on Thursday February 29, 2024 @11:02AM (#39551140)
As far as I know, it hasn't been formally verified.

Andrea Lattuada (https://andrea.lattuada.me/) is more likely to have done work in his implementation of the algorithm than I did on mine.

I have run the testing with various dynamic analysis tools, but for sure this isn't formal verification. If someone is interested in doing it, happy to chat with them!

[ Parent | on HN ]
Re:A lock-free ring-buffer with contiguous reservations (2019) by anonymousDan on Thursday February 29, 2024 @05:40PM (#39556190)
Shouldn't be that hard to at least model check it in TLA+ I would have thought (albeit potentially more complex if trying to account for weak memory).
[ Parent | on HN ]