Bengt Jonsson and Kostis Sagonas: Testing and Verifying Concurrent Algorithms Using Stateless Model Checking

In this talk we 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.


Bengt JonssonBengt Jonsson is a professor of Computer System at Uppsala University. He received his M.Sc. from Stanford University in 1985, and his Ph.D. from Uppsala University in 1987. His research has concerned semantics, specification, verification, and testing of concurrent, parallel, and embedded computer systems. He has been initiate and director of several larger research efforts at Uppsala University: the competence center ASTEC (Advanced Software Technology) between 1995-2005, and the Linnaeus Center of excellent UPMARC (Uppsala Multicore Architecture Research Center) in 2008-2018. He has served in various roles at he Swedish REsearch council, and was a co-recipient of the CAV award (on Computer Aided Verification) in 2017.

 

 Kostis Sagonas is an Associate Professor at the the Department of  Information Technology of Uppsala University. His research interests  are in programming language and software technology. His Ph.D. thesis
work was in the implementation of tabling in logic programming. In the last fifteen years he has been heaviily involved in the design and implementation of the concurrent functional language Erlang, having made significant contributions both to the evolution of the language  itself (in particular, he has designed its language of types and specs  and bitstring pattern matching), its runtime system and virtual  machine, its native code compiler (HiPE, ErLLVM), and to static  analysis and transformation tools for the language (Dialyzer, TypEr and Tidier). In the last few years he has been working on developing  novel techniques and tools for testing concurrent programs  (Concuerror, PropEr, CutEr, Nifty, Target and Nidhugg), and the ArgoDSM system for scalable software distributed shared memory.