Tutorial: How to Test and Verify Programs and Protocols with Concuerror

Debugging concurrent programs is often quite hard. There is lament about how difficult it is to reproduce a known bug, a lot of guessing about the exact causes and often one has to settle with a fix that "may not completely solve the problem".

Concuerror is a tool designed to make the process of finding, reproducing and fixing such bugs easy: given any Erlang program as input, it explores all interleavings of the processes involved, focusing smartly on pairs of "racing" events and even popping hints about what the user can do to make the search more effective. If any process crashes, Concuerror will print a detailed log of the events that lead up to the crash and will also allow the developer to visually explore the interleaving.

You may have already seen one some video or tutorial on what Concuerror can do on some (small) programs.  However, this tutorial will go deeper. After explaining what Concuerror can do for testing concurrent programs, we will also describe how one can use the tool to model, test and verify distributed protocols.  Special emphasis will be given on what a user can do to use the tool most effectively.

More info on Concuerror: http://parapluu.github.io/Concuerror

Adventures in Corfu: Testing and Verifying Chain Repair Protocols using Concuerror

Corfu is a picturesque island in Greece which is located immediately to the north of the two Paxos islands. It's considerably larger island than the Paxos ones, more involved and, arguably, much more interesting.

Corfu also happens to be a consistency platform designed around the abstraction of a shared log. The Corfu infrastructure provides this shared log to clients, which use the log for coordination, communication and storage. Corfu is a variant of Chain Replication and, in this context, one needs to worry about chain repairs: how repair of a failed node can be performed after a node restarts in a way that preserves the key properties that need to hold in this context: immutability and linearizability.

In this talk we will briefly present Corfu (the consistency platform that is, not the island) and we will describe experiences from using Erlang to model chain repair methods for Corfu and from using Concuerror to test and verify the correctness of these methods.

This is recent joint work with Stavros Aronis and Scott Lystig Fritchie.

Slides
Video

About Kostis

Kostis Sagonas is an academic who has been heavily involved in the development of Erlang and its implementation since 1999. At Uppsala University, he led the development team of the HiPE native code compiler that nowadays is part of Erlang/OTP. Together with his students, first at Uppsala University and more recently at the National Technical University of Athens, he has proposed various changes and additions to the language (most notably: bit-level pattern matching and bit-stream comprehensions, and the language of type and spec declarations) and has contributed to its compiler and runtime system. Besides HiPE, he has designed and implemented software development tools for Erlang (dialyzer, typer, tidier, proper, ...) and has contributed bug fixes to many open-source Erlang projects.

 

GitHub: kostis

Back to conference page