3 ms·
Spin: Formal verification of multi-threaded code
- spin_fan 2y agoSpin is my new favorite thing. It helped me learn Paxos by model checking the algorithm. My writeup/getting started guide here (for checking Paxos) https://github.com/glycerine/spin_paxos https://github.com/glycerine/spin_paxos It is kind of awesome that you can alter the algorithm and immediately look at the counter example (problem you just created).
- spin_fan 2y agoSpin is a great learning tool. Spin is so much more accessible than TLA+ Toolbox, for instance. But for really serious work, there are much more modern approaches that exploit SMT solvers like Z3 (as TLA+ does) for vastly more powerful model checking than Spin offers. Also, the creator of Spin has retired it seems; email to the spin list bounces. The "community" forum has not accepted registrations for several years. Basically it seems Spin was a one man show, and he has not passed the torch onto anyone else. The tool is still incredible though, and a great place to start. Just don't expect any help if you get stuck. Get the Spin book if you want to understand all the options. Here, for example, EPR is a vastly more powerful formalism: I just watched this video from 2017 work, and was blown away. They can model check FULL Vertical Paxos (not just a single round of Synod) in that same couple of seconds; that was done for the first time in this paper. Paxos Made EPR: Decidable Reasoning about Distributed Protocols Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham. OOPSLA 2017. (pdf) https://arxiv.org/pdf/1710.07191.pdf https://arxiv.org/pdf/1710.07191.pdf (video) https://youtu.be/_suyrSMJeCo https://youtu.be/_suyrSMJeCo (from the first author's homepage)