-
Notifications
You must be signed in to change notification settings - Fork 1
/
DPOR_README
210 lines (154 loc) · 8.7 KB
/
DPOR_README
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
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
Optimal Dynamic Partial Order Reduction for Analysis of Concurrent Programs
---------------------------------------------------------------------------
Contents:
---------
1. Introduction
2. Prerequisites
3. Quick intro
4. Tests
5. Interesting details in the code
1. Introduction
---------------
The purpose of this readme file is to offer a brief guide around an
experimental version of the Concuerror tool, which was developed to include an
algorithm for optimal partial order reduction of the state space generated by
the exploration of concurrent applications written in the Erlang language.
The experimental functionality, as well as two more similar
extensions/modifications are enabled with command line options. The tool runs
the stable version, if these are not provided. The stable version supports a few
more Erlang built-in functions that require preemption points and has been
tested and integrated with a GUI. The experimental versions use the command line
interface.
2. Prerequisites
----------------
Concuerror is an Erlang application, so you will need an Erlang runtime system
to run it. Most Linux distributions have suitable packages. To run the original
Concuerror testsuite you will also need Python. The application startup and
shutdown relies on a bash script, so it is currently not possible to run
Concuerror on a Windows machine.
You can build the application using 'make'
3. Quick intro
--------------
Concuerror expects as input a set of Erlang source modules, a target function
and a preemption bound. Its output in results.txt are all the traces of the
program that had some concurrency error.
We explain each briefly the command line options:
- source files : are the files that will be instrumented to include preemption
points before built-in functions that may affect the global
state.
Option: -f <files>
- target function : is an exported function in one of the files given as
input. This is the function that will be run by the first
process.
Option: -t <Module> <Name> [<arg1> <arg2>] (arguments are optional. If none is
given, the function with 0 arity
will be called)
- preemption bound : designates how many 'unnecessary' preemptions are allowed
in the current run. Concuerror will always allow enabled
processes to run after a process has become blocked (by
trying to execute a receive when no matching messages are
in its mailbox) and will also allow processes to be
interrupted while still being enabled for other processes
to be scheduled instead as many times as the preemption
bound.
Option: -p <number or 'inf' for infinite bound> (default value is 2)
- versions : by default you will be running the stable version of
Concuerror. The following command line options can be used to
enable 3 alternative versions, based on the same machinery:
--dpor_fake : is a 'sanity' check version of Concuerror using the
modified scheduler, but treating all operations as
dependent. Should give results similar to those of
the stable version, with maybe a few more
interleavings.
--dpor : is our experimental extension. Uses simple source sets to
decide additional interleavings, together with our set of
rules for dependencies between Erlang built-in functions.
--dpor_flanagan : is a version using the algorithm proposed by
Flanagan and Godefroid, extended with sleep sets
as described in our cited paper.
Examples:
To run stable Concuerror on two modules test.erl and foo.erl in your home
directory, using test:run/0 as your starting function and infinite preemption
bound:
./concuerror -f ~/test.erl ~/foo.erl -t test run -p inf
To run the same test using our experimental extension:
./concuerror -f ~/test.erl ~/foo.erl -t test run -p inf --dpor
You can run ./concuerror --help for description of a few more command line
options.
4. Tests
--------
You can instantly run two different testsuites that showcase the experimental
version:
a) The dpor_tests collection
b) Concuerror's stable testsuite, which has been adapted slightly to run the
experimental version instead of the stable one.
Let's go into more details:
a) dpor_tests
-------------
This is a collection of motivating examples that were used during the
development of the experimental version. They include toy Erlang programs as
well as all the examples presented in the paper. The toy tests were written to
expose dependencies in the supported Erlang built-in functions and to showcase
the differences and strengths between the different versions of the tool.
The tests output is compared against a stored expected output to decide success
or failure. A few (less than 5, usually 1) of the tests are expected to fail: in
these cases a diff of the expected output and the real output should show
environment related changes, as the traces sometimes include information that is
environment sensitive.
These tests are in the dpor_tests directory and you can run all of them by:
dpor_tests/dpor_test
... and a specific test by:
dpor_tests/dpor_test dpor_tests/dpor_test/src/<test>.erl
The output is written in the dpor_tests/new_results directory and is compared
with the reference output in dpor_tests/results. If it differs the test is
reported as FAILED and the output is left for comparison. You can then use a
(graphical) diff tool (e.g. meld) to see the differences in the outputs.
You can of course run any of the tests with e.g.:
./concuerror -f dpor_tests/src/<test>.erl -t <test> <test> -p inf --dpor
Interesting tests in dpor_tests:
--------------------------------
- ets_dependencies.erl : This is the simple 2 readers vs 1 writer example.
- ets_dependencies_n.erl : This is the extended example presented in the paper.
You can run this example with a varying number of readers <N> like this:
T=ets_dependencies
./concuerror -f dpor_tests/src/$T.erl -t $T $T <N> -p inf --dpor
- file_system_example.erl : The file system example written in Erlang
- independent_receivers.erl : A test with just two interleavings, where stable
Concuerror explores 234300 interleavings.
- register_again.erl : A test showing usage of Erlang built in functions.
- ring_leader_election_symmetric : An implementation of leader election in a
set of processes connected in a ring.
- ring_leader_election_symmetric_buffer.erl : Same as before, with the
difference that here mailboxes are 'modeled' as separate processes in such a
way that 'sends' and 'receives' are also interleaved, leading to an
explosion in the number of explored interleavings.
- send_it_ets.erl : An example showing why send operations with the same message
to the same process must be also interleaved.
b) Concuerror's stable testsuite
--------------------------------
Concuerror's stable testsuite has also been run with --dpor to check for any
missing dependencies. The files are stored in testsuite/suites, including
reference results. Running the tests creates the testsuite/results (which can
again be diffed against the reference directory in case of failures).
You can run the suite by:
make test
87 of the tests are expected to fail because the reference results are those
obtained by running --dpor_fake. This is to show the difference, which in most
cases favors --dpor (unless an unsupported instruction is used, in which case
the program crashes).
The --dpor_fake results are in the dpor directories under each suite. They have
been compared against the results (stored in the vanilla directories) obtained
by running the stable version with a few added preemption points. These are in
turn comparable with the original results (stored in the results directories).
Interesting test in Concuerror's testsuite
------------------------------------------
- manolis_test_2workers: Corresponds to the rush_hour test presented in the
paper.
5. Interesting details in the code
----------------------------------
Apart from concuerror_rep.erl which has all the replacement functions for the
actual calls that are found in the instrumented modules, all the main algorithm
run from concuerror_sched.erl. The dependent/2 boolean function returns true
when two operations are dependent. The main loop of the algorithm is in the
explore/1 function. Finally the two different DPOR versions differ in the details
of add_all_backtracks/1 function.