50
J. ˇ
Svejda et al.
even though they rarely finish without a considerable headroom until the limit
of 90 seconds. On average, nitwit is about 4.2 times faster than the runner up
FShell-witness2test, 17.8 times than CPA-witness2test, 22.0 times than
CPAchecker, 35.3 times than Ultimate Automizer and 39.1 times than
MetaVal.
Validator
Result
Witnesses
Mean
Median
Std.dev.
Total
nitwit
False
8526
0.63
0.02
4.74
5393
All
11533
0.64
0.02
4.99
7386
FShell-witness2test
False
7005
2.67
1.30
5.90
18734
All
11533
3.93
1.40
12.69
45337
CPA-witness2test
False
6104
11.21
8.40
8.90
68407
All
11533
13.62
8.60
15.59
157037
CPAchecker
False
7642
13.87
11.00
11.29
105968
All
11533
26.02
12.00
30.88
300145
Ultimate Automizer
False
4393
22.23
16.00
16.03
97640
All
11533
28.57
16.00
28.01
329488
MetaVal
False
1681
24.66
17.00
17.81
41453
All
11533
63.12
96.00
39.82
728008
Table 1: Runtime statistics for validators (in seconds).
Figure 4(b) shows the memory usage in successful validations plotted on a logscale with data sorted again in ascending order. nitwit needed the least (5 MB
on average; maximum 1 GB) RAM, closely followed by FShell-witness2test.
The validators were only rarely approaching the limit of 7 GB (black line at
the top); the largest value slightly above 4 GB during a successful validation
was exhibited by CPA-witness2test. The tools do not suffer from a lack of
available memory, which is also demonstrated by the low rate of Out of memory
results in Figure 2.
All validations. Figures 4(c) and 4(d) demonstrate the resource consumption of
all validations. Until about the 10 500
th witness, nitwit remains consistently
faster than all other validators, usually finishing under one second. Then, it
struggles to find the answers as some witnesses do not resolve enough nondeterminism or contain very long or even infinite paths.
Compilation-based FShell- and CPA-witness2test avoid the overhead of
an interpreter, so are mostly able to finish before the 90 second mark, because
even if the harness they extract is incomplete (still contains nondeterminism),
then after compilation the execution ends quicker than if it were interpreted. In
terms of absolute numbers, nitwit takes an average 0.64 seconds per witness
on the whole dataset with a median of 0.02 and standard deviation 4.99. The
runtime difference on average is 3.3 seconds in favor of Nitwit compared to
FShell-witness2test and 13.0 seconds to CPA-witness2test. More interesting is the median though, this was 0.02 seconds, 1.4 seconds, 8.6 seconds,
J. ˇ
Svejda et al.
even though they rarely finish without a considerable headroom until the limit
of 90 seconds. On average, nitwit is about 4.2 times faster than the runner up
FShell-witness2test, 17.8 times than CPA-witness2test, 22.0 times than
CPAchecker, 35.3 times than Ultimate Automizer and 39.1 times than
MetaVal.
Validator
Result
Witnesses
Mean
Median
Std.dev.
Total
nitwit
False
8526
0.63
0.02
4.74
5393
All
11533
0.64
0.02
4.99
7386
FShell-witness2test
False
7005
2.67
1.30
5.90
18734
All
11533
3.93
1.40
12.69
45337
CPA-witness2test
False
6104
11.21
8.40
8.90
68407
All
11533
13.62
8.60
15.59
157037
CPAchecker
False
7642
13.87
11.00
11.29
105968
All
11533
26.02
12.00
30.88
300145
Ultimate Automizer
False
4393
22.23
16.00
16.03
97640
All
11533
28.57
16.00
28.01
329488
MetaVal
False
1681
24.66
17.00
17.81
41453
All
11533
63.12
96.00
39.82
728008
Table 1: Runtime statistics for validators (in seconds).
Figure 4(b) shows the memory usage in successful validations plotted on a logscale with data sorted again in ascending order. nitwit needed the least (5 MB
on average; maximum 1 GB) RAM, closely followed by FShell-witness2test.
The validators were only rarely approaching the limit of 7 GB (black line at
the top); the largest value slightly above 4 GB during a successful validation
was exhibited by CPA-witness2test. The tools do not suffer from a lack of
available memory, which is also demonstrated by the low rate of Out of memory
results in Figure 2.
All validations. Figures 4(c) and 4(d) demonstrate the resource consumption of
all validations. Until about the 10 500
th witness, nitwit remains consistently
faster than all other validators, usually finishing under one second. Then, it
struggles to find the answers as some witnesses do not resolve enough nondeterminism or contain very long or even infinite paths.
Compilation-based FShell- and CPA-witness2test avoid the overhead of
an interpreter, so are mostly able to finish before the 90 second mark, because
even if the harness they extract is incomplete (still contains nondeterminism),
then after compilation the execution ends quicker than if it were interpreted. In
terms of absolute numbers, nitwit takes an average 0.64 seconds per witness
on the whole dataset with a median of 0.02 and standard deviation 4.99. The
runtime difference on average is 3.3 seconds in favor of Nitwit compared to
FShell-witness2test and 13.0 seconds to CPA-witness2test. More interesting is the median though, this was 0.02 seconds, 1.4 seconds, 8.6 seconds,