C subset

This page describes the C subset act expects as input. Certain parts of act, such as the C command, natively understand this subset; other parts just assume it, and generally won't work with C that doesn't comply with it. Generally, the subset is an intersection of Memalloy and Herd's respective assumptions and restrictions.

Note: The subset is liable to change constantly as we decide which fuzzing strategies to do; in addition, this page is liable to be outdated and incomplete. The final arbiter of what act considers acceptable C is the C.Mini module.

Allowed types

Currently:

• int
• atomic_int

Global variables

In compilable C, the shared-memory variables are atomic_ints declared in the translation unit, and may take initialisers. In C/Litmus, they instead appear in the Litmus init block, with the usual Litmus syntax requirements (and also in the functions; see below)

// Compilable C
atomic_int x = 0;
atomic_int y = 0;

// Litmus
{
  x = 0;
  y = 0;
}

Functions

The translation unit should consist of n functions returning void, each labelled P0, P1, and so on. In compilable C, these should take zero arguments; in C/Litmus, they should take an atomic_int* for each shared variable.

// Compilable C
void
P0()
{
  // ...
}

// Litmus
void
P0(atomic_int *x, atomic_int *y)
{
  // ...
}

Statements

Currently implemented in act:

• assignments of expressions to lvalues (variables or pointer indirections *);
• atomic_store_explicit;
• if statements;
• empty expression statements.

Expressions

Currently implemented in act:

• integer constants;
• atomic_load_explicit;
• address-taking (&, but only as the source of an atomic load, or destination of an atomic store.