What is C4?
C4 is a project to check C compiler concurrency. The goal is to be able to find bugs in the way real-world compilers implement the C11 memory model.
Our approach is based on several key principles:
- Interesting concurrency bugs are
nondeterministic , so our approach is designed around sets of states not singular outcomes - Litmus tests are the
de facto standard for concurrency testing, so our approach harmonises with them - Test cases should combine both interesting concurrent behaviour and compiler tar-pits
- We can get a lot of mileage by using existing tools in unusual ways
The C4 subprojects
C4 contains several free and open-source (FOSS) subprojects:
- c4f
- a fuzzer for litmus tests github; MIT with some CECILL-B code
- c4t
- an automatic runner for compiler test campaigns github; MIT
- c4-corpora
- a set of litmus tests pre-generated with memalloy, for use as c4f input github; public domain
- c4-scripts
- a set of Bash scripts for automating some c4f and c4t workflows github; MIT
- mutated-llvm
- a copy of LLVM instrumented with run-time selectable, concurrency-related, mutations github; Apache 2.0 with LLVM extensions
These projects are designed to be used together with a litmus test runner (such as litmus7) to run automatic tests against compilers on one or more machines.
Running tests with C4
Documentation on how to use C4 is forthcoming - watch this space!
Getting involved
We have a roadmap for future development priorities.
We welcome contributions for each of the subprojects, be they code changes, documentation, or examples and case studies. Check each subproject's GitHub repository to find out more.
Publications
- Andrei Lascu, Matt Windsor, Alastair F. Donaldson, Tobias Grosser, John Wickerson: Dreaming up Metamorphic Relations: Experiences from Three Fuzzer Tools. MET@ICSE 2021: 61-68
- Matt Windsor, Alastair F. Donaldson, John Wickerson: C4: the C compiler concurrency checker. ISSTA 2021: 670-673
Acknowledgements
Development on C4 was funded from 2018 to 2021 as part of Interface Reasoning for Interacting Systems.