- Author
- Lorin Hochstein (Surfing Complexity)
- Published
- 22 September 2024
- Kind
- Personal blog explainer with TLA+ models and code in a linked repository
- Original
- surfingcomplexity.blog/2024/09/22/linearizability-refinement-prophecy/
- Subject
- Checkable specs for coding agents
- Themes
- Checking the work, Getting good
What it is
Lorin Hochstein writes a blog on software, complex systems and incidents. The post explains a result from Herlihy and Wing's linearizability paper and Lamport's book. The author says explaining is the best way to learn.
What it says
- Hochstein describes a spec as a state machine: initial states plus allowed transitions.
- A data structure is linearizable if each operation appears to take effect instantly.
- To show an implementation meets a spec, map its states onto the spec's states.
- Herlihy and Wing's array queue admits no such mapping, though it is linearizable.
- Adding a prophecy variable that predicts dequeue order lets the mapping exist.
- Wrong predictions only block dequeues or cause deadlock, which stays a valid behavior.
What evidence it gives
The post works through counter, queue, locked-list and array-queue examples with diagrams. It shows excerpts of PlusCal, Python and C++ code. Full TLA+ models are in two linked GitHub repositories. The post does not report running the models.
Interests and limits
The post is a personal explainer. The author says readers may not absorb it at first. The full prophecy mapping is deferred to Lamport's book. The post leaves liveness out. Model checking results are not reported. The figures were images, which were not viewed.
Connections
These links are this wiki's own reading, not claims the sources make.
- The Decoherence Trap: When AI slop drowns out the signal in an endless sea of noise. Maevyn describes locally valid models that no longer fit together. Hochstein shows a formal remedy on one queue: map one model's states onto another's. The map sometimes needs an invented prophecy variable. How large a system could afford such maps?
- Girls Just Wanna Have Fast MPMC Queues with bounded waiting. Nahla's post carries a correction: the queue is not wait-free after all. Hochstein walks through what proving a related property takes, on a small queue. Would a model have caught the slip sooner?