I have to thank @Hillelogram here for introducing his Twitter following to TLA+. The whole concept doesn't look that wild, but even just a superficial knowledge of it just helped me out by a surprising amount
Started playing around with TLA+ a few days ago, wrote a 70 line spec today (this would probably be a lot shorter if I actually knew what I was doing), and while it didn't show me a fundamental flaw in my system, it helped me realize and check that some mutexes were redundant.
The point is not that I couldn't have convinced myself of the correctness without TLA+, it's rather that I probably would have been too lazy, but with the spec already written, I could just change a few things, rerun the model checker, and gain confidence that this works
(spec is in PlusCal, desierd properties written in TLA+. Making sure that removing the locks doesn't break anything is a bit tricky because of how steps work in TLA+, but for small projects you can just add labels everywhere in your PlusCal if statements are atomic)
PlusCal doesn't have a native concept of mutexes or condition variables (nor does TLA+), but I was able to model those with macros of two or three lines each.
While there are some TLA+ and PlusCal examples that implement mutex algorithms, I didn't find anything about proving properties on algorithms that use mutexes or cvs. In the end it wasn't complicated, but took some time to figure out.
I guess I'm not really using #tlaplus at the same abstraction levels everyone else seems to be using it, so this might not come up often, but I'd be interested in hearing other experiences with modelling multithreaded algorithms.
I might also write a blog post about how I use TLA+ once I get a bit more experience. Providing a small library or some examples of how to argue about systems that use multithreading primitives like blocking queues seems like fun
On the other hand, @Hillelogram probably already covered all of this in his new book. Will have to get that as soon as it comes out.
