Download

The checker can be downloaded here

Compile the checker

The checker is written in C#, compliant with .NET framework version 1.1, Mono 1.1.10.1

- Using Visual Studio .NET 2003: Load the solution file mmchecker.sln into the IDE and compile.

- Using Mono: Compile all .cs files in the project using the command mcs -recurse:src -out:mmchecker.exe

Run the checker

The checker can be run from the command line

mmchecker.exe <name>.test

where as <name>.test is the file contains details for the checker to run the test

How to write a .test file ?

The .test file contains multiple lines with format attribute=value. For example

memorymodel=csharp.mm
program=peterson
observer=SimpleCumulativeObserver
search=maxflow

• memorymodel specifies the file containing specification for the memory model that the checker uses to check the program.
• program specifies the bytecode file, it should be generated from .NET .exe binary by the tool ildasm.exe from .NET framework SDK.
• observer is an attribute for furture development, should be set to SimpleCumulativeObserver now.
• search specifies the method of checking, it can assume a number of value:
  - maxflow: find barrier insertion positions
  - full: only do a full reachability analysis
  - guided: guided execution to make the execution follow the path specified in guided_path attribute: a list of numbers showing which transition to take at each successive state.
• print_execution=1 specifies that the virtual machine should print details about each step it takes.
• trace=1 puts the checker in interactive tracing mode, allowing the user to view the current state and select the next transition to be executed.

The memory model file

The memory model is specified in the non operational/executable using a table showing whether two bytecodes can be reordered under the memory model. The text file contains an array of 7x7 number assuming values either 0 or 1 to indicate whether a reordering of two operation op1 and op2 is allowed according to their semantics. A number 1 in line i column j indicates that if op1 has i^th semantic and op2 has j^th semantic then op1 and op2 can be reordered. The 7 semantics are: none, read, write, volatile read, volatile write, lock and unlock.

The two files csharp.mm and sc.mm is provided in the package for C# and Sequential Consistency model. Of course sc.mm only contains 0s because no reordering is allowed under sequential consistency.

Specifying the invariant

The program to be checked needs to be compiled together with mmc.cs which is included in the package. The class MMC defined in the file allows specifying the invariant by the function call MMC.Report(int).

For example, if we need to check the variable counter at the end of the program, we add a call MMC.Report(counter) in the source code at the location the program halts. The checker will do a reachability analysis to find all possible values of counter under Sequential Consistency and C# memory model; and if counter can have more values in C# memory model than Sequential Consistency, the checker will find places to put Thread.MemoryBarrier() in order to disallows these behaviours.

In order to check for an invariant, for example (counter==2), we can call MMC.Report((counter==2)?1:0) so that if the invariant is violated, the expression will have value 0 and otherwise.

Interpreting the output

Consider the output from the run with the Double-checked locking (dc) test, the explanation is in italic:

(7): 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
Good end values: 7
-- Above are the analysis for Sequential consistency, in which the variable only assumes value 7
-- The string after the value show one execution trace that leads to the value
(7): 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
(0): 0 0 0 0 0 0 1 1 1 1 2 0 0 0 0 0 0 0 0 0 0 0 0
-- Next is the analysis for C# memory model, in which the variable can get a new value 7
Done, running maxflow algorithm with 229 vertices 479 edges
Ford-Fulkerson: 98
-- The maxflow algorithms finds a cut with capacity 98
method GetHelper ()::IL_001e: stfld class Helper DoubleCheck::helper
-- One barrier needs to be inserted before the instruction labeled IL_001e in method GetHelper()
SC time: 00:00:00.1602304
CE time: 00:00:00.1402016
FR time: 00:00:00.3805472
MF time: 00:00:00.0400576
Total : 00:00:00.4206048
-- SC: Sequential Consistent check time, CE: First counter example in C# time
-- FR: Full reachability analysis in C#, MF: Maxflow algorithm time
REPORT:3: 1 0 0 0 0 0 0 2
State count: 228
-- There are total 228 states in the state space under C# memory model