-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
155 lines (134 loc) · 6.2 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
<!DOCTYPE html>
<html lang="en-GB">
<head>
<meta charset="utf-8">
<link rel="preconnect" href="https://fonts.gstatic.com">
<link href="main.css" rel="stylesheet">
<title>The C4 Project</title>
<meta name="description" content="A project for testing and exploring the low-level concurrency behaviour of real-world C compilers.">
</head>
<body>
<header>
<img src="logo.svg" id="logo" alt="C4 logo">
<h1>The C4 Project</h1>
<p>Explosive Compiler Concurrency Testing</p>
</header>
<main>
<section id="what-is">
<h2>What is C4?</h2>
<aside id="diagram">
<object type="image/svg+xml" data="workflow.svg">
</object>
</aside>
<p>
<abbr title="C Compiler Concurrency Checker">C4</abbr> is a project to <em>check C compiler concurrency</em>.
The goal is to be able to find bugs in the way <em>real-world</em> compilers implement the C11 memory model.
</p>
<p>
Our approach is based on several key principles:
</p>
<ul>
<li>Interesting concurrency bugs are <emph>nondeterministic</emph>, so our approach is designed around sets of states not singular outcomes</li>
<li>Litmus tests are the <emph>de facto</emph> standard for concurrency testing, so our approach harmonises with them</li>
<li>Test cases should combine both interesting concurrent behaviour and compiler tar-pits</li>
<li>We can get a lot of mileage by using existing tools in unusual ways</li>
</ul>
</section>
<section>
<h2>The C4 subprojects</h2>
<p>
C4 contains several free and open-source (FOSS) subprojects:
</p>
<dl>
<dt><a href="c4f.html">c4f</a></dt>
<dd>
a fuzzer for litmus tests
<span class="coderef">
<a href="https://github.com/c4-project/c4f">github</a>; MIT with some CECILL-B code
</span>
</dd>
<dt><a href="c4t.html">c4t</a></dt>
<dd>
an automatic runner for compiler test campaigns
<span class="coderef">
<a href="https://github.com/c4-project/c4t">github</a>; MIT
</span>
</dd>
<dt>c4-corpora</dt>
<dd>
a set of litmus tests pre-generated with
<a href="https://github.com/johnwickerson/memalloy">memalloy</a>,
for use as c4f input
<span class="coderef">
<a href="https://github.com/c4-project/c4-corpora">github</a>; public domain
</span>
</dd>
<dt>c4-scripts</dt>
<dd>
a set of Bash scripts for automating some c4f and c4t
workflows
<span class="coderef">
<a href="https://github.com/c4-project/c4-scripts">github</a>; MIT
</span>
</dd>
<dt>mutated-llvm</dt>
<dd>
a copy of LLVM instrumented with run-time selectable,
concurrency-related, mutations
<span class="coderef">
<a href="https://github.com/c4-project/mutated-llvm">github</a>; Apache 2.0 with LLVM extensions
</span>
</dd>
</dl>
<p>
These projects are designed to be used together with
a litmus test runner (such as
<a href="http://diy.inria.fr">litmus7</a>) to run
automatic tests against compilers on one or more machines.
</p>
</section>
<section>
<h2>Running tests with C4</h2>
<p>
Documentation on how to use C4 is forthcoming -
watch this space!
</p>
</section>
<section>
<h2>Getting involved</h2>
<p>
We have a <a href="roadmap.html">roadmap</a> for
future development priorities.
</p>
<p>
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.
</p>
</section>
<section>
<h2>Publications</h2>
<ul>
<li>
Andrei Lascu, Matt Windsor, Alastair F. Donaldson, Tobias Grosser, John Wickerson:
<a class="publication" href="https://doi.org/10.1109/MET52542.2021.00017">Dreaming up Metamorphic Relations: Experiences from Three Fuzzer Tools</a>.
MET@ICSE 2021: 61-68
</li>
<li>
Matt Windsor, Alastair F. Donaldson, John Wickerson:
<a class="publication" href="https://doi.org/10.1145/3460319.3469079">C4: the C compiler concurrency checker</a>.
ISSTA 2021: 670-673
</li>
</ul>
</section>
<section>
<h2>Acknowledgements</h2>
<p>
Development on C4 was funded from 2018 to 2021 as part of
<a href="https://interfacereasoning.com">Interface Reasoning for Interacting Systems</a>.
</p>
</section>
</main>
</body>
</html>