My Authors
Read all threads
This is exactly the right question to ask. I’ve been talking about this with a few people lately. I actually think it goes both ways. There are two challenges: ensuring the spec specifies a practical implementation, and ensuring the code correctly implements the spec. (1/?)
This was the first spec I’ve written that really encountered the first challenge. I initially modeled some operations in a single step that in the implementation would have been problematic as it would have required a mutex around a database (consensus) call.
So I had to refactor the spec to model the potential for the OS to reorder concurrent operations, and that change was critical as it exposed what would have been significant defects had the spec been implemented without the mutex, as it should (ideally) be.
The second challenge is ever present, and I wish I had a good solution for it. But in most cases I’ve found my implementations do become more complex than my specs because they’re constrained by libraries and semantics, making it more difficult to verify the impl is correct.
For example, this spec requires that cached entries be retained until the database has propagated events up to the entry version (logical time) to avoid reordering reads following an eviction. But the LRU cache library I used in the implementation doesn’t support that behavior.
The implementation uses a separate Go map to store recent entries that need to be retained in addition to the LRU cache for entries that can safely be evicted. These kinds of inevitabilities can make the eyeball test difficult, but the idea of an eyeball test is itself a problem.
In my recent conversations, one strategy I’ve seen for gaining confidence in the impl was doing Jepsen style verification of histories, which is an idea I like. Another suggestion was to simply keep the impl of the spec minimal, perhaps using a direct translation of the steps.
But all of these solutions still make me uneasy. Formal methods can only be used to create correct systems when they have correct implementations. And while we have the tools to gain confidence in a TLA+ spec, it’s not always easy to guarantee the implementation matches the spec.
I’m still in the process of updating the impl with the latest changes in the spec, but given the small size and complexity of the algorithm, I am confident I’ll be able to produce an implementation that’s consistent with the spec even considering the language/library limitations.
So maybe there is something to be said for limiting the scope of the spec and size of the impl. But that’s difficult with more complicated specs. And even with a limited scope, I’m still fallible. Without a verifiable programming language there’s always a risk I make an error.
Missing some Tweet in this thread? You can try to force a refresh.

Enjoying this thread?

Keep Current with Jordan Halterman

Profile picture

Stay in touch and get notified when new unrolls are available from this author!

Read all threads

This Thread may be Removed Anytime!

Twitter may remove this content at anytime, convert it as a PDF, save and print for later use!

Try unrolling a thread yourself!

how to unroll video

1) Follow Thread Reader App on Twitter so you can easily mention us!

2) Go to a Twitter thread (series of Tweets by the same owner) and mention us with a keyword "unroll" @threadreaderapp unroll

You can practice here first or read more on our help page!

Follow Us on Twitter!

Did Thread Reader help you today?

Support us! We are indie developers!

This site is made by just three indie developers on a laptop doing marketing, support and development! Read more about the story.

Become a Premium Member ($3.00/month or $30.00/year) and get exclusive features!

Become Premium

Too expensive? Make a small donation by buying us coffee ($5) or help with server cost ($10)

Donate via Paypal Become our Patreon

Thank you for your support!