PULSE ProTest User Level Scheduler for Erlang

Copyright © Quviq AB, 2009-2017.

PULSE is a randomizing scheduler for Erlang, which can be used to find race conditions in concurrent Erlang code. It was initially developed at Chalmers University under the ProTest project (www.protest-project.eu) by the ProTest research group, consisting of Thomas Arts, Koen Claessen, John Hughes, Michal Palka, Nick Smallbone and Hans Svensson--see our paper at ICFP 2009--and released under a BSD licence. This version has been extended and integrated into QuickCheck by Quviq.

Concurrency errors

PULSE is used to increase the possibility to find concurrency errors as well as to improve the analysis of these errors by offering the ability to create random schedulings and rerun the same scheduling deterministically.

In order to use PULSE, one needs to instrument the code under test by compiling it with a special flag (see pulse_instrument). After that, the concurrent processes are run by calling pulse:run/1. Note that one may need to start the application pulse first (which will start QuickCheck).

As an example, consider the following "hello world" function:
helloworld() ->
  Self = self(),
  ForwardPid = 
	  spawn(fun() ->
		        receive Msg -> Self ! Msg end
  spawn(fun() -> Self ! hello, ForwardPid ! world end),	
	   M1 -> 
		      M2 -> [M1,M2]

This program sends two messages to a receiving process, which returns the messages in the way they arrived. Note that on a one core computer, the result is very predictable and always the same. However, when you port this program to a multi-core machine, you may now and then see a different execution behaviour. For larger programs, this gets more evident. In fact, when you would run each of the processes in a separate Erlang node, one would indeed see more often different orders of the two incoming messages.

The Erlang scheduler, however, is too deterministic to find more than one order in which the messages arrive and hence simple unit tests like
[hello,world] = helloworld().

would pass and let the developer believe the program has this behaviour.

When the "hello world" program is compiled with PULSE, then it can be evaluated by using more random schedules.

1> pulse:start().
2> pulse:verbose([all]).
3> pulse:run(fun() -> examples:helloworld() end).
PULSE scheduling started
root spawns 'helloworld.ForwardPid' <0.1360.0> at {"examples.erl",47}
root spawns helloworld <0.1361.0> at {"examples.erl",52}
root blocks at {"examples.erl",56}
helloworld sends hello to root at {"examples.erl",53}
helloworld sends world to 'helloworld.ForwardPid' at {"examples.erl",54}
helloworld terminated normal
'helloworld.ForwardPid' blocks at {"examples.erl",48}
helloworld delivers world to 'helloworld.ForwardPid'
'helloworld.ForwardPid' receives world at {"examples.erl",49}
'helloworld.ForwardPid' sends world to root at {"examples.erl",49}
'helloworld.ForwardPid' terminated normal
'helloworld.ForwardPid' delivers world to root
root receives world at {"examples.erl",57}
root blocks at {"examples.erl",58}
helloworld delivers hello to root
root receives hello at {"examples.erl",59}
return value [world,hello]
PULSE scheduling finished
The output is in textual form and its verbosity can be adjusted via pulse:verbose/1. Visualization as a graph is supported if graphviz is installed by using the event handler. PULSE does send by default all events to an event handler (pulse_event_terminal). By adding an extra event handler, one can send teh same events also to the pulse_event_graph event handler, making it into a graph.

4> gen_event:which_handlers(pulse_event).
5> gen_event:add_handler(pulse_event,pulse_event_graph,[]).
6> pulse:rerun().

When used with QuickCheck, the macro ?PULSE is recommended. This macro has the same shape as the ?FORALL macro, i.e., ?PULSE(Result,Generator,Property) where the generator is a function that is evaluated with a certain schedule, Result is the result of the function and this can be used in the property.

prop_helloworld() ->
           Result == [hello,world]).

Generated by EDoc, Sep 18 2017, 16:17:35.