Small Datum

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 l imited 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 w

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 t