Generating input

act expects a certain format of input; this page gives tips on how to generate it.

Assembly input

Refer also to the list of supported architectures.

act makes the following assumptions about the assembly:

• The assembly file contains a contiguous run of subprogram code where each subprogram starts with a label containing either Pn (where n is a non-negative number), or a label that act can recognise as a compiler-mangled form of Pn (eg _P0);
• All subroutine calls and returns can be ignored;
• All stack pointer manipulations can be ignored (though act will generally translate stack locations to symbolic heap locations, assuming that each stack offset corresponds to a single and unique location for each thread);
• All directives can be ignored.

C input

To get the right assembly input, the C input should follow a specific format:

• The C file should contain several functions of the form void Pn() { /* ... */ }, where the only function calls are to <stdatomic.h> atomic actions;
• All variables should be global, in the form tXrY (where X is the program number and Y is a number unique within thread X);
• Any other code (for example, main methods and thread running harnesses) should be conditionally compiled (and act told not to compile it, through compiler flags).

Input for the test command

The test command expects, as input, a directory containing:

• a C/ directory containing *.c files (as above);
• a litmus/ directory containing, for each X.c in the above, a corresponding C11 litmus test with the name X.litmus.

This deliberately follows the structure of memalloy results output (see below).

Using memalloy

Recent versions of the dev branch of memalloy produce the format act needs. An example invocation that gives useful output is:

./comparator -arch C -violates models/c11_lahav.cat -satisfies models/c11_normws.cat -events 4 -iter

(Note that the default Herd model is weaker than c11_lahav, and thus produces some false positives. A Herd7 compatible version of c11_lahav is forthcoming.)