See the following paper for the theory behind the conversion:
We have two conversions: an eager conversion which is simple, but guesses global valuations that may not be reachable, and a more involved lazy conversion that converts in such a way that all reachable states of the sequential program correspond to reachable states of the concurrent program.
The Linux binaries for the two conversions are available:
Context switches |
Eager | Lazy | |||||||||||||||||||
4 processes: 2 adders and 2 stoppers
(cbp file)
1 |
bp file |
bp file |
2 |
bp file |
bp file |
3 |
bp file |
bp file |
4 |
bp file |
bp file |
5 |
bp file |
bp file |
6 |
bp file |
bp file |
|
Here is a summary of experimental results on these Bluetooth examples (the resulting sequential programs were run on Moped).
Context switches |
Reach? | Eager time(s) |
Lazy time(s) |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
2 processes: 1 adder and 1 stopper
1 |
No |
0.1 |
0.1 |
2 |
No |
0.3 |
0.2 |
3 |
No |
43.3 |
1.4 |
4 |
No |
73.6 |
5.5 |
5 |
No |
930.0 |
20.2 |
6 |
No |
- |
66.8 |
|
3 processes: 2 adder and 1 stoppers
| 1 |
No |
0.2 |
0.1 |
2 |
No |
0.9 |
0.8 |
3 |
No |
135.9 |
6.3 |
4 |
Yes |
1601.0 |
2.6 |
5 |
Yes |
- |
18.0 |
6 |
Yes |
- |
122.9 |
|
3 processes: 1 adders and 2 stopper
| 1 |
No |
0.1 |
0.1 |
2 |
No |
0.7 |
0.9 |
3 |
Yes |
70.1 |
0.4 |
4 |
Yes |
597.2 |
2.9 |
5 |
Yes |
- |
14.0 |
6 |
Yes |
- |
66.1 |
|
4 processes: 2 adders and 2 stoppers
| 1 |
No |
0.2 |
0.1 |
2 |
No |
1.6 |
2.0 |
3 |
Yes |
177.6 |
0.8 |
4 |
Yes |
Out of memory |
7.5 |
5 |
Yes |
Out of memory |
66.5 |
6 |
Yes |
Out of memory |
535.9 |
|