I've implemented something similar to one of my employers:
- We had existing lockfree MPMC stack/queue/etc data structures in C.
- I've converted existing code to PlusCal almost 1-to-1 to best of my ability. There were some nitpicks regarding how PlusCal implements return values, so I took some liberties. But important part is from a view of sequential consistency, most if not all sequence points were preserved. That is a bit weak guarantee as obviously every C sequence point potentially compiles to multiple instructions, so one could go and model instructions directly if that is what required. But most lockfree algorithms are not relying on specific ordering of instructions between threads, they more relying on ordering of sequence points, so overall it's fairly ok.
- On top of that I've added a "test program" written also in PlusCal that emulates 2-3+ threads and tries to add/remove elements from the data structure, test program keeps a separate set of "correct" elements. And it compares reference to result of algorithm.
- Then I've limited generation counters (common feature in lockfree algorithms to resolve ABA) to something small like 100.
- Running TLC then finds all possible states, and proves that algorithm is correct, with exception of generation counter wrap around (if one thread is stuck and another wraps around generation counter, then you still arrive at ABA).
Generally it's great for sequential consistency code. My next goal was to try different relaxed memory models, but I've moved to other stuff ..