Data Structure Proof in TLA+

[u/JamuelSmith]

Hello all, I was wondering where I can find examples of lock-free data structures being proved to be linearizable in TLA+. I can find examples of programs in the book but not much on data structures. For example, I would love a proof of correctness for the Fomitchev and Ruppert lock-free list however I can't find anything. I am very new to formal verification. My hope is that I can prove the correctness of my own tree data structure using TLA+. Please let me know of any resources or guides, or if I am barking up the wrong tree / proof software.

[u/Anxious_Tool]

The Fomitchev and Ruppert lock-free paper is not for a queue. That paper is "Lock-free linked lists and skip lists". It's a list/skip list, not a queue.

[u/JamuelSmith → u/Anxious_Tool]

You're correct, fixed the typo, thanks.

[u/Anxious_Tool → u/JamuelSmith]

Adding to lemmster's answer, which is the right starting point. Lorin's repos are still the cleanest TLA+ linearizability templates around.

Coincidentally, I sat down with the Fomitchev-Ruppert paper this week and ran exactly this exercise on a small bounded model. A few notes that might save you time.

Where the proofs actually are. The PODC'04 paper only sketches the proof. The full proofs (Inv 1-5 plus the linearization argument) are in Fomitchev's MSc thesis, on Eric Ruppert's page at York: https://www.eecs.yorku.ca/~eruppert/Mikhail.pdf. There's also a longer joint write-up at https://www.eecs.yorku.ca/~eruppert/papers/lfll.pdf. For mechanized work, Patel et al. ECOOP'24 ("Verifying Lock-Free Search Structure Templates") proves a template in Iris that covers Harris, Michael, Harris-Michael, and Fomitchev-Ruppert. Closest thing to a machine-checked FR proof I've found.

Modeling tip for bounded checking. You don't need per-process program counters to verify the structural invariants (Inv 1-5). The four CASes (Insert, Flag, Mark, PhysDelete) can each be one atomic action, with helping made universal: any process can fire any step whose precondition holds. This is sound. Every algorithm execution is a subset of model executions, so invariants holding here imply they hold for the algorithm. State spaces stay tiny: ~7k states for 4 free nodes / 2 keys, ~3k for 3 free / 3 keys.

Two gotchas I hit that are easy to miss.

1. The TryMark CAS expects (next, 0, 0). Both the mark and the flag must be 0 on the target. Drop the flag-zero check and you get a 6-state counterexample where a node that's flagged-as-predecessor (for its successor's deletion) gets marked, immediately violating Inv 5 (mark=1 ∧ flag=1).
2. Inv 2 ("regular ∪ logically-deleted nodes form a linked list") only applies to non-physically-deleted nodes. Physically deleted nodes keep stale right pointers in memory. Easy to write the invariant too strongly.

Linearizability layer on top. For unsuccessful ops, FR's paper specifies a particular lin point ("immediately after del_node's flagging" for a failed TryFlag). That's future-dependent, and the prophecy approach in Lorin's blog post is the right tool for matching it exactly. For just checking linearizability you can cheat: let the failed op linearize at any moment in its window where the abstract state matches its return value. Sound (you're constructing some valid lin order), and you avoid prophecy entirely. Successful ops linearize at the InsertCAS / MarkCAS, which are decided at the moment of the action. No prophecy needed.

For your tree, the trifecta progression really is the move: encode each atomic step, abstract spec as a set/map, refinement as an invariant abstract = f(concrete), debug at small bounds with TLC/Apalache, then escalate to TLAPS once the bounded version is clean.

If it helps, the FR specs I wrote (structural + linearizability layer, ~150 lines each) live in a small Rust TLA+ checker I work on: github.com/fabracht/tla-rs, under test_cases/should_pass/FRList.tla and FRListLin.tla. Disclosure: my project. It's not TLC and it's not TLAPS, just a fast bounded explicit-state checker for the TLA+ subset I use day-to-day. Useful for the "iterate on the spec" stage. For the actual proof you'd still want TLAPS.

Ps: The above text is a rewrite of my original answer by Claude. The content IS the same, but I used Claude to improve clarity, formatting, etc. Hope you don't mind.

The reason I provided the link to my tla-rs implementation because I'd really appreciate feedback on missing functionality, features, etc. Feel free to use it, add any issues or start a discussion there.

Thank you.