fond
Model Checking Contest @ Petri Nets 2013
Milano, Italy, June 25, 2013
Facts About the MCC’2013
Last Updated
Apr. 26, 2013

Introduction

This page summarizes some facts about the elaboration of the MCC'2013.

The Models

This section provides some data about the models tools had to process:

“Known” Models “Surprise” Models
231 models 24 models
CSRepetitions (Colored, 6 instances)
CSRepetitions (P/T, 6 instances)
Dekker (P/T, 6 instances)
DotAndBoxes (Colored, 4 instances)
DrinkVendingMachine (Colored, 2 instances)
DrinkVendingMachine (P/T, 2 instances)
Echo (P/T, 9 instances)
Eratosthenes (P/T, 8 instances)
GlobalRessAlloc (Colored, 7 instances)
GlobalRessAlloc (P/T, 2 instances)
Kanban (P/T, 8 instances)
LamportFastMutEx (Colored, 7 instances)
LamportFastMutEx (P/T, 7 instances)
MAPK (P/T, 6 instances)
NeoElection (Colored, 7 instances)
NeoElection (P/T, 7 instances)
PermAdmissibility (Colored, 6 instances)
PermAdmissibility (P/T, 6 instances)
Peterson (Colored, 6 instances)
Peterson (P/T, 6 instances)
Philosophers (colored, 13 instances)
Philosophers (P/T, 11 instances)
PhilosophersDyn (colored, 5 instances)
PhilosophersDyn (P/T, 3 instances)
RessAllocation (P/T, 15 instances)
Ring (P/T, 1 instance)
RwMutex (P/T, 12 instances)
SharedMemory (colored, 14 instances)
SharedMemory (P/T, 6 instances)
SimpleLoadBal (colored, 5 instances)
SimpleLoadBal (P/T, 5 instances)
TokenRing (colored, 7 instances)
TokenRing (P/T, 4 instances)
HouseConstruction (P/T, 8 instances)
IBMB2S565S3960 (P/T, 1 instance)
QuasiCertifProtocol (Colored, 6 instances)
QuasiCertifProtocol (P/T, 6 instances)
Vasy2003 (P/T, 1 instance)

In total, each tool was confronted against 17 examinations applied on 255 models/instances, so a total of 4335 examinations. We performed semi-automatic analysis from the outputs provided by these executions.

The table below shows a summary of the characteristics of these models.

The Computers

Three computers were made available to operate the submitted tools. Since the computers have some differences in their characteristics, we processed all the examinations of all the instances of a model on the same machine to let us measure comparable data.

A short description of these machine is provided in the table below.

cluster1 (Univ P. & M. Curie) ebro (Univ. Rostock) quadhexa-2 (Univ. Nanterre)
CPU
total of 46 CPU total of 64 CPU total of 24 CPU
23 x Intel Xeon E5645
2.4 GHz, 6-Core, 6x 1536KB/12288KB L2/L3
4 x AMD Opteron™ 6200 Series (Interlagos)
2.7 GHz, 16-Core, 16x 1024KB/16MB L2/L3
4 x Intel Xeon X7460
2.66 GHz, 6-Core, 3 x 3MB/16NB L2/L3
Memory
23 x 8GB (2x4GB) DDR3 / PC1333 512GB (32x 16GB) DDR3 / PC1600 128BG (8x 16BG) DDR3 / PC1333
Disks
23 x 500GB SATA 7200 +
1TB SATA 7200
2 x 1TB SAS2-Server-RAID +
2 x 128GB SSD Samsung 830 SERIES SATA III MLC
4 x 400GB RAID 1 (mirror) Seagate SAS Cheetah
Linux Kernel
2.6.38.8-server-10.mga 2.6.32-358.11.1.el6.x86_64 3.8.1-server-1.mga3

In fact, we used:

The organizers thank the Universities of Paris-Ouest-Nanterre, Rostock and Pierre & Marie Curie for letting us using their computers.

The executions

This section provides some data about the executions of the examinations over the proposed benchmark, for both the “Known” and the “surprise” models. Please note that the number of execution does not includes a large number of preliminary tests in cooperation with the tool developers.

“Known” Models “Surprise” Models
Confinement of the Execution
Memory : 4GB
CPU : 2700s
Memory : 4GB
CPU : 2700s
Total Number of tool executions (one examination on one model instance)
49380 4913
Execution per Machine
cluster1 (Univ P. & M. Curie) : 24937
quadhexa-2 (Univ. Nanterre) : 24443
ebro (Univ. Rostock) : 1640
quadhexa-2 (Univ. Nanterre) : 3273
Total CPU Time required
80 days, 18 hours, 17 minutes, 11 seconds 3 days, 11 hours, 45 minutes, 12 seconds
Size of collected raw data (CSV, outputs, etc. excluding charts)
1,77GB 122,3MB
Produced Performance Charts (for models)
1182 177
Produced Execution Charts (for relevant executions)
13763 1541