Litmusify

The litmusify command takes a C or assembly file and converts it to a litmus test, suitable for consumption by herd or litmus. It allows one-shot investigation of single files, in contrast to test, which performs a full test cycle.

Synopsis

$ act litmusify [FLAGS] (-compiler COMPILER_ID | -arch ARCH_NAME) FILE

Details

If the input file is C, act runs the compiler associated with the compiler ID, then processes the resulting assembly as if it were passed to litmusify directly. This requires -compiler; -arch won't work.

Flags

litmusify takes the standard flags, as well as the following:

Mandatory

• One of -compiler COMPILER_ID or -arch ARCH_ID, where COMPILER_ID is any compiler ID in the configuration file, and ARCH_ID is any of the supported architectures. Note that act can only explain a C file if given a -compiler.

Optional

• -sanitiser-passes PREDICATE: modifies the set of sanitiser passes act runs before outputting the litmus test (see the sanitiser page for details).
• -c or -asm: overrides act's default file type behaviour, which is to consider the input as C if its name ends in .c, or assembly otherwise.
• -herd or -litmus: pipes the litmus test to the configured herd or litmus tool, and substitutes its output for the litmus test.
• -c-globals GLOBALS: tells act that the given variables (given as a comma-delimited string) are global C variables, so that it can handle them appropriately in the assembly.
• -c-locals LOCALS: as above, but marks the variables as local (in the sense that herd et al. can ignore them when outputting state sets).

Variable format

For -c-globals and -c-locals, the format of each item in the comma-separated list is n:NAME=VAL, where n is a thread ID, NAME is the name of the variable, and VAL is an initial value. Both n: and =VAL can be omitted (generally, n: makes sense only for locals, and =VAL for globals). Variables without n: are presumed not to refer to any thread's local variables, and variables without =VAL are presumed to start with value 0.