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 Stavros

Stavros finished his master's degree at NTUA, Greece with a thesis on the implementation of an extension for Dialyzer’s type system. He is currently studying towards a PhD degree in Uppsala University, doing research on Erlang tools. He has developed the parallel version of Dialyzer and is the main developer and maintainer of Concuerror.

GitHub: aronisstav

Twitter: @Vahnatai

Back to conference page