Skip to main content.

Experimental evaluation of DiVinE Tools

The overall goal of DiVinE is to efficiently utilize available computational resoururces to complete its verification task or complete it sooner. The efficiency of selected DiVinE Tools is reported in the following several case studies.


DiVinE Cluster on DAS-3

In this experiment we evaluated performance of algorithms MAP and OWCTY as implemented in DiVinE Cluster. Our primary aim was to show that the tool can scale up to 256 CPU cores. Our performance evaluation was done on the Distributed ASCI Supercomputer (DAS-3), a wide-area distributed system for Computer Science research in the Netherlands. The casestudy was done by Kees Verstoep from VU University, Amsterdam.

Distributed ASCI Supercomputer (DAS-3)

DAS-3 consists of five clusters distributed over four sites. It uses Myri-10G networking technology from Myricom both as an internal high-speed interconnect as well as an interface to remote DAS-3 clusters. DAS-3 is largely homogeneous: every cluster uses dual-CPU AMD Opteron nodes, but with different clock speeds and/or number of CPU cores. For the purpose of this experiment we employ DAS-3 cluster at VU University, which has the largest number of compute nodes and cores (85 nodes with a dual-cpu, dual-core 2.4 GHz AMD Opterons).

Intitial experiments on DAS-3 were performed with DiVinE Cluster version 0.7.2 that contained several performance flaws due to which an efficient usage of the tool was limited to clusters with small number of nodes (less than 20). However, we succeed to optimize the tool to efficently employ much larger number of cores that were available on DAS-3 system. The optimized implementation reffered below corresponds to the DiVinE Cluster version 0.8 (will be released shortly).

Experiments on Scalability and Efficiency

First, we show graphs depicting the scalability of unoptimized and optimized implementations. For the purpose of this experiment, we run DiVinE Cluster on anderson.8.prop.dve model from BEEM database. Each line in the graphs below shows scalability for the given number of nodes when using 1 core per node, 2 cores per node, and 4 cores per node.

MAP Scalability OWCTY Scalability

To get an estimate on the efficiency of MAP and OWCTY, we ran single-core versions on a special DAS-3/VU node equipped with 16GB memory (the regular compute nodes have 4GB, which is insufficient to store the state space there). The efficiencies of optimized implementations are quite good even for 256 cores. In particular, MAP on a single core took 1052.5 sec; the runtimes on 64, 128, and 256 cores are 23.0, 13.1, and 8.9 sec, giving efficiencies of 72%, 63% and 46%, respectively. OWCTY on a single core took 631.7 sec; the runtime on 64, 128, and 256 cores are 13.3, 7.4 and 5.0 sec, giving efficiencies of 74%, 67% and 49%, respectively. The results are shown in the two following tables.

MAP Efficiency OWCTY Efficiency
Cores Runtime (sec) Efficiency
1 1052.5 100%
64 23.0 72%
128 13.1 63%
256 8.9 46%
Cores Runtime (sec) Efficiency
1 631.7 100%
64 13.3 74%
128 7.4 67%
256 5.0 49%

Measuring Network Throughput

The following graphs illustrate the effect of the improvements on the applications' throughput as a function of their runtime. In this case a larger instance of the Anderson problem was used to obtain a higher resolution graph.

MAP Throughput OWCTY Throughput





DiVinE Multi-Core Performance Evaluation

The following tables reports on selected runtimes for Reachability and LTL model checking verification tasks performed using DiVinE Multi-Core version 1.1. You may also be interested in the table with all experiments.

Reported runtimes are in seconds (rounded). All models come from the BEEM database. The meassurements were performed for two different architectures:

manwe: 8x Dual Core AMD Opteron(tm) Processor 885
pheme: 2x Intel Xeon CPU 5130 @ 2.00GHz

The value X denotes that the corresponding experiment didn't complete (memory overflow).
The value -- denotes that the corresponding experiment was not performed.
The ! next to time means that a counterexample has been found before exploring full state space of the model.

Reachability (generation of all reachable states)

Model divine @ manwe_64bit

1 core2 cores4 cores8 cores16 cores
divine @ pheme_64bit

1 core2 cores3 cores4 cores
anderson.6
2:291:221:052716
2:111:115155
at.6
25:4014:087:554:122:16
20:0411:298:446:42
at.7
2:49:29 X25:28 X16:28 X11:44 X13:18 X
34:52 X5:14 X3:17 X2:48 X
bakery.6
1:354423148
1:16372620
blocks.4
16:299:134:442:391:25
13:057:154:564:01
cambridge.7
3:071:41 -- 3322
2:461:291:2658
elevator.5
30:3924:2918:2219:1718:46
24:17 X18:40 X14:20 X14:08 X
elevator_planning.2
2:171:0833169
2:021:014231
firewire_link.6
2:15:04 X1:52:44 X30:47 X12:53 X5:19 X
34:43 X20:05 X7:21 X6:51 X
frogs.5
51:1319:5910:195:153:06
35:0315:0611:038:14
iprotocol.7
7:414:112:111:1240
6:34 -- 3:112:17
lamport.8
9:074:512:301:2343
7:234:042:442:12
lann.7
35:5018:189:385:162:46
29:0414:4510:3710:48
lann.8
2:12:03 X32:43 X15:50 X0 X5:11 X
24:23 X8:05 X4:59 X4:06 X
leader_filters.6
25:0312:405:533:091:43
17:40 X8:31 X6:534:24 X
loyd.3
1:04:0330:0313:497:203:33
41:4211:37 X5:38 X6:47 X
peg_solitaire.3
15:06:33 X3:30:19 X1:12:51 X31:56 X13:04 X
2:22:41 X34:44 X19:48 X14:44 X
peterson.7
24:0011:386:143:111:48
19:069:226:415:21
phils.8
14:107:554:132:281:41
11:044:40 X2:25 X1:41 X
sokoban.3
13:5512:2212:2412:2413:42
10:09 X10:16 X10:09 X10:15 X
szymanski.5
13:056:194:443:082:23
11:085:356:114:21
telephony.5
1:53:4843:39 X32:2617:339:20
40:07 X6:18 X3:41 X3:34 X
train-gate.7
6:005:021:561:0936
5:092:46 -- 2:18

LTL Model checking

Model divine @ manwe_64bit

1 core2 cores4 cores8 cores16 cores
divine @ pheme_64bit

1 core2 cores3 cores4 cores
anderson.6.prop2 (valid)
8:404:573:302:101:30
7:144:053:072:52
anderson.6.prop4 (valid)
11:416:274:462:451:56
9:395:234:103:56
elevator.5.prop3 (valid)
49:2138:1629:5630:4532:04
16:35 X10:44 X7:05 X7:15 X
elevator2.3.prop4 (valid)
9:275:403:282:071:35
8:184:513:503:05
elevator2.3a.prop4 (valid)
1:2956352114
1:18473429
lamport.7.prop4 (valid)
23:1213:238:105:163:39
19:4110:588:286:49
lann.8.prop2 (n/a)
1:26:43 X20:32 X10:03 X6:04 X0 X
21:17 X5:13 X3:16 X2:40 X
lann.8.prop3 (n/a)
1:32:48 X20:01 X9:46 X6:00 X3:09 X
22:49 X5:10 X3:07 X2:36 X
leader_election.5.prop2 (valid)
4:453:342:091:1147
4:17 -- 2:011:53
leader_election.6.prop2 (valid)
43:00 -- 16:1610:498:28
38:3612:08 X5:40 X6:13 X
leader_filters.6.prop2 (valid)
1:06:1637:0521:4215:5411:06
12:35 X5:03 X3:16 X2:33 X
leader_filters.7.prop2 (valid)
9:045:103:082:251:45
7:34 -- 3:232:53
mcs.5.prop4 (valid)
36:3622:4213:278:366:14
31:0610:53 X8:56 X7:26 X
peterson.5.prop4 (valid)
1:38:1852:5832:1220:2013:35
26:06 X4:27 X3:09 X2:45 X
peterson.7.prop4 (valid)
1:51:4658:4836:1822:4015:41
26:22 X7:49 X5:55 X4:19 X
public_subscribe.5.prop1 (n/a)
1:20:41 X22:36 X10:17 X5:13 X2:41 X
20:30 X5:41 X3:29 X2:37 X
rether.5.prop5 (valid)
1:271:00322220
1:15 -- 3928
rether.7.prop5 (valid)
2:221:12583827
2:061:055855
szymanski.4.prop4 (valid)
1:2051393328
1:09433935
anderson.3.prop2 (invalid)
35:57 -- 14:3410:268:20
-- -- -- --
at.4.prop2 (invalid)
3:3314 !3 !2 !1 !
2:5012 !2 !0 !
bakery.5.prop2 (invalid)
4:00 -- 1:311:0243
3:181:491:211:10
bakery.6.prop2 (invalid)
7:0610 !1 !0 !3 !
5:469 !1 !2 !
elevator.5.prop2 (invalid)
1:28:301:12:422:48 !1:08 !4 !
17:07 X7:29 X6:22 X2:23 !
iprotocol.4.prop4 (invalid)
3:092:111:2910 !54
2:361:341:201:11
lamport.6.prop2 (invalid)
2:06 !8 !0 !0 !0 !
1:41 !7 !0 !0 !
lann.6.prop3 (invalid)
1:57:4924:56 !39:4426:2119:18
25:22 X7:05 X5:33 X4:20 X
peterson.5.prop2 (invalid)
1:43:0214:20 !36:1623:4917:14
27:27 X4:23 X2:21 !1:40 !
phils.6.prop2 (invalid)
6:462:39 !52 !3 !0 !
5:422:21 !1:16 !50 !
szymanski.5.prop2 (invalid)
1:00:527:34 !1:20 !8 !3 !
23:59 X6:32 !3:36 !54 !
rether.5.prop6 (invalid)
1:342 !0 !0 !0 !
1:202 !0 !0 !