Verified Certification of Reachability Checking for Timed Automata
439
seem to be an obvious way to improve on this situation for SML implementations.
Finally, one can see that the verified certifier is not drastically slower than the
unverified implementation based on Mlunta, indicating that the verified certifier
is not missing any obvious significant optimizations.
Certifier for #threads
Model
Size Uppaal Tandem Munta Unverif. 1-MLton
1
2
3
4
FDDI
8
0.33
0.79 1.01
0.14
0.21 0.99 0.64 0.57 0.53
10
5.93
1.77 2.50
0.40
0.45 2.13 1.36 1.26 1.20
12
92.66
3.93 5.42
0.90
1.20 3.41 2.33 2.25 2.18
14 1874.28
7.28 10.73
1.86
2.22 5.36 3.94 3.90 3.88
16
***
12.80 19.51
3.47
3.72 11.09 6.49 6.50 6.51
FDDI broad 8
0.34
0.28 1.07
0.10
0.08 0.26 0.19 0.17 0.16
Fischer
5
0.24
2.78 6.33
0.72
0.53 1.76 1.07 0.98 0.91
6
34.74 143.72 377.70
40.99
26.58 40.60 25.47 24.16 23.67
CSMA
5
0.04
0.94 4.42
0.31
0.28 1.44 0.87 0.80 0.76
6
1.53
13.48 65.16
5.24
4.18 12.16 8.04 7.87 7.76
Mode
Pacemaker
1
0.02
0.16 0.37
0.03
0.03 0.25 0.16 0.14 0.13
2
0.02
0.75 3.20
0.17
0.26 1.23 0.75 0.68 0.65
3
0.03
1.39 4.23
0.34
0.46 2.53 1.55 1.40 1.31
4
0.02
11.80 0.70
3.24
3.71 12.13 8.38 6.69 6.66
5
0.02
30.84 0.86
9.13
10.07 26.60 18.58 18.15 17.95
Table 1: Benchmarks results on a machine with 16 GB RAM and an Intel(R) Core(TM)
i7-4610M CPU at 3.00GHz with two cores and two threads per core. The column
labeled “Tandem” gives the runtime for a combination of the unverified SML tool and
the verified certificate checker. The next column gives the runtime of the unverified
SML certifier, followed by the runtimes of the verified checker for a varying number of
threads. All times are given in seconds.
Table 2 gives the results of evaluating the different compression algorithms
on the same set of benchmarks. The second variant is always applied to the
compression result of the first variant to avoid trivial computations of the
convex hull. Variant 2c) (the most expensive one) can produce drastically smaller
certificates than any other variant, and its minimum compression factor is an
order of a magnitude higher than for any other variant. Nevertheless, only variants
1 and 2a) appear to be useful in practice, as they are relatively cheap to compute.
The other variants could prove useful if the certificates were produced by a
significantly more efficient model checker, such as Uppaal or TChecker [15]. On
a final note, we have constructed a more than 95% smaller but valid certificate
for the Fischer benchmark, suggesting that there is room for improvement on
the compression algorithms.
439
seem to be an obvious way to improve on this situation for SML implementations.
Finally, one can see that the verified certifier is not drastically slower than the
unverified implementation based on Mlunta, indicating that the verified certifier
is not missing any obvious significant optimizations.
Certifier for #threads
Model
Size Uppaal Tandem Munta Unverif. 1-MLton
1
2
3
4
FDDI
8
0.33
0.79 1.01
0.14
0.21 0.99 0.64 0.57 0.53
10
5.93
1.77 2.50
0.40
0.45 2.13 1.36 1.26 1.20
12
92.66
3.93 5.42
0.90
1.20 3.41 2.33 2.25 2.18
14 1874.28
7.28 10.73
1.86
2.22 5.36 3.94 3.90 3.88
16
***
12.80 19.51
3.47
3.72 11.09 6.49 6.50 6.51
FDDI broad 8
0.34
0.28 1.07
0.10
0.08 0.26 0.19 0.17 0.16
Fischer
5
0.24
2.78 6.33
0.72
0.53 1.76 1.07 0.98 0.91
6
34.74 143.72 377.70
40.99
26.58 40.60 25.47 24.16 23.67
CSMA
5
0.04
0.94 4.42
0.31
0.28 1.44 0.87 0.80 0.76
6
1.53
13.48 65.16
5.24
4.18 12.16 8.04 7.87 7.76
Mode
Pacemaker
1
0.02
0.16 0.37
0.03
0.03 0.25 0.16 0.14 0.13
2
0.02
0.75 3.20
0.17
0.26 1.23 0.75 0.68 0.65
3
0.03
1.39 4.23
0.34
0.46 2.53 1.55 1.40 1.31
4
0.02
11.80 0.70
3.24
3.71 12.13 8.38 6.69 6.66
5
0.02
30.84 0.86
9.13
10.07 26.60 18.58 18.15 17.95
Table 1: Benchmarks results on a machine with 16 GB RAM and an Intel(R) Core(TM)
i7-4610M CPU at 3.00GHz with two cores and two threads per core. The column
labeled “Tandem” gives the runtime for a combination of the unverified SML tool and
the verified certificate checker. The next column gives the runtime of the unverified
SML certifier, followed by the runtimes of the verified checker for a varying number of
threads. All times are given in seconds.
Table 2 gives the results of evaluating the different compression algorithms
on the same set of benchmarks. The second variant is always applied to the
compression result of the first variant to avoid trivial computations of the
convex hull. Variant 2c) (the most expensive one) can produce drastically smaller
certificates than any other variant, and its minimum compression factor is an
order of a magnitude higher than for any other variant. Nevertheless, only variants
1 and 2a) appear to be useful in practice, as they are relatively cheap to compute.
The other variants could prove useful if the certificates were produced by a
significantly more efficient model checker, such as Uppaal or TChecker [15]. On
a final note, we have constructed a more than 95% smaller but valid certificate
for the Fischer benchmark, suggesting that there is room for improvement on
the compression algorithms.