Formal methods in the real world

A lot of interesting work is done at Amazon but not much is written about it. There is an article on their use of formal methods via TLA+ and PlusCal. I haven't seen much use of formal methods in my career. I have spent a lot of time debugging code written by other people, so I wouldn't mind if such tools were used more frequently.

I used the Spin tool for two MySQL features. I hope other people try the tool and read the book. I first used it when we rewrote the InnoDB RW-lock at Google. The RW-lock had an awkward implementation that limited performance on many-core and many-socket servers. The new implementation was (mostly) lock free and inspired by the excellent work of Yasufumi Kinoshita. We used Spin to verify that the state transitions were probably correct. I use the word probably because Spin was used to explore the state space to find deadlocks and assertion failures. This wasn't a formal proof of correctness. We shared the Spin model with the InnoDB team when contributing the code. Our change made it into upstream InnoDB and that was one step in making MySQL better for many-core servers.

I used Spin a second time while implementing admission control for MySQL. I used a lock-free protocol to maintain per-user counts of running queries. This was done to avoid mutex contention and the code was more complex than using atomic increment/decrement. I re-read the Spin book prior to writing the Spin model and think I was better at it than during my first project.