-
Notifications
You must be signed in to change notification settings - Fork 1
Litmus tests
Matt Windsor edited this page Jan 4, 2019
·
1 revision
Litmus tests are a (de facto) standard for describing 'small parallel program[s] designed to exercise the memory model of a parallel, shared-memory, computer'. Since memalloy generates litmus tests, and both herd and litmus consume litmus tests, act
includes support for the litmus test format.
Litmus tests generally contain:
- a header, stating the language of the test and the name of the test;
- an initialisation block, setting the initial values of any shared variables;
- several programs in the previously named language;
- (potentially) a locations block, specifying which shared variables are in use;
- (potentially) a postcondition, specifying the condition for the test to pass.
The format of the programs depends on the language:
- for C, we give each program as a separate C function;
- for assembly languages, we give the programs together in a table format.
The litmus top-level module contains act
's support for the Litmus language.