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.

NOTE: The documentation on this wiki refers to the dev branch of act, not master. This is a temporary distinction: dev is a branch to which I'm committing things that depend on travesty-0.5.1, and will go away once travesty updates in OPAM. (End of NOTE)

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.
• The C subset act understands internally.

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

Running tests

These are the main test drivers; they combine many of the tasks done by the smaller sub-commands in the process of running tests.

• Compare: compare litmus output across compilers.
• Test: test compilers using Herd and a Memalloy-style input corpus.

Manipulating single C files and litmus tests

• C: various utilities for dealing with C files and C litmus tests; most of these expect input in the known C subset.
  • C Delitmus: convert a C litmus test into a compilable C11 program.
  • C Explain: dump various facts about a C file or litmus test.
  • C Fuzz: experimental and unfinished mutation of C litmus tests.

Manipulating single assembly files and litmus tests

• Asm: various utilities for dealing with assembly files and assembly litmus tests; many commands also accept C files, given a compiler, and run the compiler first before proceeding as normal.
  • Asm Explain (formerly explain): annotate an assembly file with act's analysis.
  • Asm Litmusify: convert a single assembly file to a litmus test.

Setting up and testing act

• Configure: various tools for dealing with act configuration.
• Regress: regression tests (used mainly by act's build process).

Miscellaneous

• Tool: run external tools like Herd and Litmus directly.
  • Tool Herd: run Herd.
  • Tool Litmus: run Litmus on the local machine.

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
• Filters: act's usual abstraction for processes that take file input and return file output
• 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