Personal tools
You are here: Home Events Milner Lectures Milner Lecture 2011

Milner Lecture 2011

Milner Lecture 4pm Tuesday 21 June
Appleton Tower, LT2
The University of Edinburgh
11 Crichton Street, Edinburgh, EH8 9LE

*Followed by a reception in Informatics Forum

Finding Race Conditions in Industrial Erlang Code by Property-Based Testing
John Hughes
Chalmers University, Gothenburg
Quviq AB, Gothenburg

Race conditions bedevil concurrent programs, leading to
hard-to-replicate Heisenbugs that are near impossible to find. The
Erlang progamming language mitigates the problem by restricting
data-structures to be immutable, and outlawing shared data between
processes, but race conditions can and do still occur in real
systems. In this talk I shall explain our approach to the problem
using QuickCheck, our property-based testing tool, which uses a formal
specification to generate test cases and as a test oracle, and
simplifies failing tests to minimal counterexamples to aid fault
diagnosis. Using a form of serializability as the specification,
QuickCheck is able to find minimal examples that provoke races with
relatively little work.

QuickCheck was recently applied to the data storage layer of mnesia,
the database management system distributed together with Erlang, which
is heavily used in real applications. Our approach quickly revealed
five separate race conditions, some of which may explain Heisenbugs
that are known to occur every month or two in production systems.

If time permits, I shall also discuss current work on controlling the
scheduling of Erlang programs to make race conditions easier to

John Hughes

John Hughes is a long-time researcher in the area of functional
programming, a contributor to the design of Haskell, and author of
"Why Functional Programming Matters", one of the most widely read
articles in the area. In 2000 he and Koen Claessen developed
QuickCheck, an influential specification-based testing tool which last
year received the ACM SIGPLAN Award for Most Influential Paper of ICFP
2000. In 2006 he founded Quviq AB, which develops and markets a
commercial version of QuickCheck for Erlang, and in 2007 received the
Erlang User of the Year award as a result. Today he divides his time
between Quviq and a Chair at Chalmers University of Technology in
Gothenburg, with a research focus on the interplay of functional
programming and software testing.

Document Actions