Home

act (automagic compiler tormentor) is a toolbox for testing whether compilers respect the C memory model, based on the herd memory model testing system and the memalloy C memory model witness generator.

Information for users

Also see the README.

General information

• Supported architectures and compilers
• Configuration
• Generating input
• Standard flags accepted by every subcommand.
• Filtering predicates: the syntax of -filter-compilers and -filter-machines flags.

External tools

act interfaces with several external tools (besides compilers), which need their own set-up and configuration:

• C preprocessor (for interpreting raw C files)
• Herd (for simulating C and assembly behaviours)
• Litmus (for sampling assembly behaviours from the local machine)
• Memalloy (for generating Test input)

Command documentation

• Compare: compare litmus output across compilers.
• Explain: annotate an assembly file with act's analysis.
• Litmusify: convert a single assembly file to a litmus test.
• Test: test compilers using Herd and a Memalloy-style input corpus.
• C: various utilities for dealing with C files.
• Regress: regression tests (used mainly by act's build process).

Information for developers

• Code conventions: why things are how they are
• Converting assembly to litmus: observational notes on how we might sanitise assembly output

Deep dives

These pages discuss bits of act's design in detail.

• Overall design: making sense of act's module soup
• Abstract program model: the abstract/* modules and how they work
• Language abstraction layer: the lib/Language_* modules and how they work
• Sanitiser: the lib/Sanitiser_* modules and how they work