Running the reduction-based atomicity checker

The atomicity checker provided with Σοφία attempts to determine whether all observed executions of each method in a multi-threaded program are atomic. It is based on the technique for reduction first introduced by Lipton (paper), and implements the refinements proposed by Wang and Stoller (paper). We refer the user to the linked resources for details. There are two steps to run the atomicity checker on a program.

Instrumenting for atomicity checking

The SemanticInstrumentor provides a special parameter to instrument a program for atomicity checking. When this parameter is specified, it is not necessary to provide an event description language (EDL) specification to the instrumentor; you only need to specify the name of a program list file identifying the set of classes comprising the program on which atomicity checking is to be performed. The command to invoke the instrumentor is as follows:

java sofya.ed.semantic.SemanticInstrumentor -atom -dabe list_file

The first parameter is the key parameter that instructs the instrumentor to insert instrumentation for atomicity checking. Note that this instrumentation is not different from the instrumentation normally provided by the instrumentor; the same instrumentation could be inserted by an EDL specification. This parameter is simply a shorthand to conveniently ensure that the correct instrumentation is inserted. The second parameter disables a special set of events that are not necessary for atomicity checking, to improve performance. The third parameter, as noted previously, is the list file identifying the classes to be instrumented.

When the instrumentor is run, it will instrument the specified classes and output a data file to be used by the atomicity checker. This data file will be the name of the specified program list file, with the extension replaced by 'ed.dat'. This file contains information that will be used by the SemanticEventDispatcher to dispatch the event stream.

Running the atomicity checker

Once the program is instrumented, you are ready to run the atomicity checker. The command to do this is as follows:

java sofya.apps.AtomicityChecker -md <data_file> -main <main_class> [arg1 arg2 ...]

The '-md' argument specifies the name of the 'ed.dat' file generated by the instrumentor. The '-main' argument is used to identify the class that should be used to launch the program, and can be followed by any number of arguments that should be passed to the launched program.

The output of the atomicity checker will be a list of the methods that the program executed and whether or not each method was found to be atomic on all executions during this program run.