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 agentultra on Thursday February 29, 2024 @10:57AM (#39551057)
Has there been a formal specification/model that we can check? I love circular buffers but I'm curious how we know that the design is correct with respect to the stated properties.

I did a bit of link diving to the various blog posts and sites but haven't been able to find it. Would be nice, if it exists, to have it front and centre.

[ Parent | on HN ]
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 ]