Information Technology Reference
In-Depth Information
example that provokes a fault in the software under test. Finding such minimal
failing tests is invaluable in speeding fault diagnosis. Yet our approach depends
fundamentally on being able to repeat a test, with the same result as the first
time it was run; finding minimal failing tests then requires that we can repeat
smaller tests, in the same way as the original failing test was run. In concurrent
programs, where the scheduling can vary from run to run, achieving repeatable
behaviour is already a challenge.
Our first goal is thus to enable repeatable testing of concurrent Erlang code.
This could be achieved by modifying the underlying Erlang virtual machine to
use a custom, controllable process scheduler. But in practice, users will not be
interested in using a custom version of the Erlang VM to test their systems
- in fact, many projects continue to use outdated virtual machines long after
upgrades are released, to avoid problems in their own software that might be
caused by changes in the behaviour of the VM. Thus we consider it essential
to achieve repeatable testing without changing the underlying Erlang VM. As
multicore systems become more and more prevalent, it will be less and less
reasonable to assume that the underlying scheduler can be replaced.
Our approach is instead to instrument the code under test, to make it com-
municate with a scheduler of our own design, written in Erlang, such that our
scheduler can impose purely deterministic execution on the code under test,
regardless of the underlying concurrent execution. We have developed an instru-
menting compiler (in only 400LOC) which handles almost full Erlang, and an
associated scheduler which takes control of the order of delivery of interprocess
messages. By varying this order, we can even test the behaviour of distributed
systems (which have a different semantics for message passing) on a single Erlang
node. In addition we created a way to visualize the scheduling of events, such
that the analysis of error cases becomes much easier. The scheduler currently
makes random scheduling choices, and has proven quite effective in revealing
race conditions in the examples studied so far.
6.2 Developing Model-Checking Techniques for Erlang
The other strand of work in our support for concurrency involves development of
model checking as a complementary verification technique to the use of testing.
Our initial goal was to deliver a model checker that supports a very large frag-
ment of the Erlang language (e.g., with full support for all Erlang data types,
the distributed Erlang API, and many OTP behaviours) to ease the task of
constructing a verifiable model from an Erlang program.
A prototype model checker existed at the start of the project, and we have
concentrated on delivering a number of enhancements to it, including:
-
support for model checking a much larger language fragment. To achieve this
a new source-to-source translation was realised as a number of transforma-
tions on HiPE Core Erlang code - an intermediate code level in the Erlang
compiler. In addition more OTP behaviours are handled (gen fsm, gen event,
partial support for ets tables, ...). In fact we are able to use the source code
for some Erlang/OTP modules, without changes, in model checking.
