AutoMO – Programming Languages Research Group

AutoMO: Automatic Inference of Memory Order Parameters for C/C++11

AuotMO is a tool that is able to infer memory order parameters for C/C++11 concurrent programs such that the programs only exhibit SC behaviors for the test cases provided by developers. Many concurrent data structures are initially designed for the SC memory model, and developers often implement these data structures to more relaxed memory models by adding sufficient fences to ensure that the implementation only allow SC behaviors. However, it is non-trivial to port data structures designed for the SC memory model to the C/C++11 memory model in the sense that it can become difficult and error-prone to choose the proper memory order parameters for memory operations that still allow reasonable optimization.

The key insight of AutoMO is that it utilizes a model-checker that exhaustively enumerates the executions allowed by the C/C++11 memory model, and for each execution, it checks whether that execution is equivalent to some SC execution; if not, AutoMO applies the rules based on heuristics to strengthen the memory order parameters such that it will disallow the non-SC behaviors. Also, AutoMO has a trace reordering scheme that reorders output traces to help both understand the trace and infer parameters.

The SC analysis algorithm, trace reordering analysis, and the parameter inference algorithm are described in more detail in this paper (published in OOPSLA ’15):

Getting Started

Get the source of AutoMO. We implemented AutoMO as a backend analysis of the CDSChecker model checker. If you haven’t done so already, you may download AutoMO using git:

     git clone git://plrg.eecs.uci.edu/model-checker.git

Get the benchmarks (not required; distributed separately), placing them as a subdirectory under the model-checker directory:

     cd model-checker
     git clone git://plrg.eecs.uci.edu/model-checker-benchmarks.git benchmarks

Compile CDSChecker with AutoMO backend analysis :

     make

Compile the benchmarks:

make benchmarks

Run a test case:

     ./run.sh TESTCASE_NAME [CDSChecker Options] -t AUTOMO -o [AutoMO OPTION]

Useful Options

If you are not familiar with the options of CDSChecker, PLEASE refer to the CDSChecker page first.

-o file-InputFile

Take the parameter assignments in the [InputFile] as the input of the parameter inference algorithm. The argument should be right after the symbol ‘-‘ with full directory.

-o anno

Turn on the annotation mode for the controlled non-SC behaviors (by default OFF)

-o no-weaken

Turn off the weakening process, which lets AutoMO to finish a specific search session when it infers a strong enough parameter assignment.

-o implicit-mo

Imply implicit modification order. You might only want to use this option when some execution ends in an infinite loop because specific stores have not established modification order. (by default OFF)

Running Your Own Code

If you want to use AutoMO, PLEASE follow these steps.

First of all, since AutoMO is a backend analysis of the CDSChecker, you need to follow the instructions of CDSChecker about how to write runnable test cases.

Second, you should replace the memory order parameters that you want AutoMO to infer.

To accomplish that, you will need to include our header file “wildcard.h”. This header file provides wrappers for wildcard parameters which represents the parameters to be inferred. For example, for a memory operation “x.store(***)” (the stars represent the parameter to be inferred), you will need to rewrite it as “x.store(wildcard(1))”. For the later memory order parameters to be inferred, you will need to use “wildcard(2)”, “wildcard(3)” and so on.

Since the C/C++11 memory model requires data race freedom, which means normal memory operations should have established the hb relation. In order to expose normal memory operations to AutoMO, you will need to use a special wrapper for them. For example, if you have a normal memory operation “x = 1”, you will need to rewrite it to be “x.store(1, memory_order_normal). The special memory order “memory_order_normal” is also defined in the “wildcard.h” file.

Third, compile your test cases as required in CDSChecker.

Fourth, run your test cases with AutoMO as an backend analysis. To invoke AutoMO in the CDSChecker model checker, you should use the “-t AUTOMO” option. Followed with the “-t AUTOMO”, you can use one or more AutoMO options to run the test case under AutoMO.

In most of the cases, you are fine with the above steps. However, if you want to use the annotation framework in AutoMO that allows controlled non-SC behaviors, you should follow one extra step. Include our header file “sc_annotation.h” first. For a specific operation that you want to allow non-SC behavior (usually loads), you will need to add one “SC_BEGIN();” statement before it, and one “SC_END();” statement after it. Then run it with the “-o anno” option.

An Example

1. Consider we have a simple program as follow — IRIW (independent read & independent write).

x = y = 0; // Initially

// T1 // T2 // T3 // T4

x = 1; y = 1; r1 = x; r3 = y;

r2 = y; r4 = x;

Under the SC memory model, it is obvious that the threads T3 and T4 will observe the store of x and y in a consistent order, which means the execution in which “r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0” is not allowed. However, under the C/C++11 memory model, if all memory operations have the memory order of memory_order_relaxed, such a non-SC execution is totally legitimate.

1. If you want to port this code snippet to C/C++11, you can rewrite memory operations to C/C++11 formats and prepare the test case with AutoMO parameter wrapper as follow (don’t forget the “wildcard.h” header file for the parameter wrappers):

// Initially

x.store(0, memory_order_seq_cst);

y.store(0, memory_order_seq_cst);

// T1 // T2 // T3 // T4

x.store(1, wildcard(1)); y.store(1, wildcard(2)); r1 =x.load(wildcard(3)); r3 = y.load(wildcard(5));

r2 = y.load(wildcard(4)); r4 = x.load(wildcard(6));

1. Compile the test case and run it under CDSChecker with AutoMO plugin on with the following command (suppose you compile this test case .

./run.sh test/iriw_wildcard.o -m2 -y -t AUTOMO -o no-weaken

1. The output is as follow:

The results are as the following:
Result 0:

wildcard 1 -> memory_order_seq_cst
wildcard 2 -> memory_order_seq_cst
wildcard 3 -> memory_order_acquire
wildcard 4 -> memory_order_seq_cst
wildcard 5 -> memory_order_acquire
wildcard 6 -> memory_order_seq_cst

This means that AutoMO infers one result that shows the mapping between each wildcard parameter to its inferred paraemter.

1. Suppose you already know that wildcard parameter “wildcard(1)” and “wildcard(2)” need to be memory_order_seq_cst, and you want to infer the rest of the parameters. You can have an input file as follow (let’s call the input file as input.txt):

Result 0:

wildcard 1 -> memory_order_seq_cst
wildcard 2 -> memory_order_seq_cst

Now you can use the “-o file-[FILE]” option to inform AutoMO with your input by running the following comman:

./run.sh test/iriw_wildcard.o -m2 -y -t AUTOMO -o file-./input.txt -o no-weaken

Disclaimer

We make no warranties that the output of AutoMO is free of errors. You are responsible for assuring the correctness of your software. See the GPL2 license for further disclaimers.

Please read the paper so that you understand what the tool is supposed to do.

Contact

Please feel free to contact us for more information. Bug reports are welcome, and we are happy to hear from our users.

Contact Peizhao Ou at peizhaoo@uci.edu or Brian Demsky at bdemsky@uci.edu for questions about AutoMO.

Copyright

CDSChecker is distributed under the GPL v2. See the LICENSE file for details.

Acknowledgments

This material is based upon work supported by the National Science Foundation under Grant Nos CCF-0846195, CCF-1217854, CNS-1228995, and CCF-1319786.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.