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.

Helping make MySQL better

My peers have been very busy the past few years helping to make MySQL better for web-scale deployments. Much of this effort is also good for deployments that aren't web-scale. Join us at Percona Live 2015 to learn more.

• Polyglot persistence @ FB keynote by Harrison Fisk
• WebScaleSQL keynote by Steaphan Greene
• MySQL for Facebook Messenger by Domas Mituzas
• MySQL Automation at Facebook Scale by Shlomo Priymak
• LSM Databases at Facebook by Yoshinori Matsunobu
• XDB: Shared MySQL Hosting at Facebook Scale by Evan Elias
• Online InnoDB Defragmentation by Rongrong Zhong
• Fast Master Failover without Data Loss by Yoshinori Matsunobu
• Row Based Replication and Incremental Logical Backup by Santosh Banda
• DocStore Document Database for MySQL at Facebook by Peng Tian and Tian Xia
• WebScaleSQL talk by Steaphan Greene
• WebScaleSQL BOF with Steaphan Greene. I hope other members from the WebScaleSQL effort will attend.
• RocksDB storage engine for MySQL BOF. I hope people from the core RocksDB team will attend.