Jonsson & Sagonas; Testing and Verifying Concurrent Algorithms Using Stateless Model Checking

In this talk we will report on our recent experiences in employing stateless model checking (SMC) to test and verify chain repair methods for CORFU, a distributed shared log that is designed to be scalable and reliable in the presence of failures and asynchrony.

A suitable model of a CORFU system, developed mainly by engineers at VMWare, was used to try different methods of chain repair and allowed a SMC tool to test and verify their correctness. The tool quickly found errors in the first two of these methods and, after some improvements in the tool itself, managed to verify the correctness of the third method. Besides more details about the above, we will present experiences and lessons learned from applying SMC to test and verify complex protocols and programs for
concurrent and distributed programming.