4 ms·
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 th
by agentultra 3y ago
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.
- jamesmunns 3y agoAs far as I know, it hasn't been formally verified. Andrea Lattuada (https://andrea.lattuada.me/ 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!
- anonymousDan 3y agoShouldn'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).