Rodin Performances: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Nicolas
m New page: Performance measures for the Rodin Platform. == Configurations == === Configuration 1 === System: * Intel Pentium Dual Core E2180 (2* 2 GHz) * 2 Go RAM OS: * Ubuntu 10.10 * linux kerne...
 
imported>Nicolas
 
(19 intermediate revisions by 2 users not shown)
Line 11: Line 11:
OS:
OS:
* Ubuntu 10.10
* Ubuntu 10.10
* linux kernel 2.6.35-24
* linux kernel 2.6.35-25
* GNOME 2.32.0
* GNOME 2.32.0


Line 24: Line 24:
* Helios (3.6.1)
* Helios (3.6.1)
* JUnit 4.8.1
* JUnit 4.8.1
* tests run from a freshly launched eclipse as only running user application, in UI thread, with an empty workbench.
 
=== Configuration 2 ===
 
System:
* Intel Pentium Dual Core E2180 (2* 2 GHz)
* 2 Go RAM
 
OS:
* Ubuntu 11.04
* linux kernel 2.6.38-9
* GNOME 2.32.1
 
Java:
* Java(TM) SE Runtime Environment (build 1.6.0_24-b07)
* Java HotSpot(TM) Server VM (build 19.1-b02, mixed mode)
* VM arguments
** -Xms40m
** -Xmx1200m
 
Eclipse:
* Helios (3.6.2)
* JUnit 4.8.1
 


== Benchmark Projects ==
== Benchmark Projects ==
Line 47: Line 69:
* 14 Machines
* 14 Machines
* 927 POs
* 927 POs
=== XCore ===
* 62 Contexts
* 50 Machines
* 2595 POs
=== XCore Encoding ===
* 45 Contexts
* 15 Machines
* 1370 POs


== Protocol ==
== Protocol ==


A measurement is launched using the JUnit plug-in '''fr.systerel.perf.tests'''.
A measurement is launched using the JUnit plug-in '''fr.systerel.perf.tests'''.
Tests are run from a freshly launched eclipse as only running user application, in UI thread, with an empty workbench.


Launch Configuration must include exactly the following plug-ins:
Launch Configuration must include exactly the following plug-ins:
Line 62: Line 97:


Verify that 1200 Mo are free when tests are ready for launch.
Verify that 1200 Mo are free when tests are ready for launch.
== Tests ==
=== Lexer ===
A base string is made of all standard Event-B Mathematical Language symbols, separated from each other with a space character.
The string to lex is made of the concatenation of 100000 times the base string.
The lexer is called 10 times on the string to lex.
=== Parser ===
The parser is called on formulae covering all Event-B operators:
* 43 predicates
* 140 expressions
* 7 assignments
* 1 big predicate (1750 characters)
The parsing is repeated 4000 times.
=== Builder / models only ===
The project initially contains only model files (contexts and machines).
It is built with auto provers turned off.
=== Builder + Auto Prover / models only ===
The project initially contains only model files (contexts and machines).
It is built with auto provers turned on.
=== Builder / models + proofs ===
The project initially contains models and proofs (contexts, machines, proofs).
It is built with auto provers turned off.


== Results ==
== Results ==


The following results are means of 3 successive measures.


{| class="wikitable" style="text-align:center; width:80%;"
{| class="wikitable" style="text-align:center; width:80%;"
Line 74: Line 146:
! scope=col | Rodin 1.3
! scope=col | Rodin 1.3
! scope=col | Rodin 2.0
! scope=col | Rodin 2.0
! scope=col | Rodin 2.1 (temporary results)
! scope=col | Rodin 2.1
|-
|-
| Lexer
| Lexer
Line 81: Line 153:
| 19.0 s
| 19.0 s
| 21.4 s
| 21.4 s
| 34.9 s
| 35.6 s
|-
|-
| Parser
| Parser
Line 88: Line 160:
| 17.1 s
| 17.1 s
| 39.3 s
| 39.3 s
| 17.1 s
| 17.2 s
|-
|-
| Builder / models only
| Builder / models only
Line 95: Line 167:
| 119.6 s
| 119.6 s
| 211.0 s
| 211.0 s
| 32.3 s
| 30.9 s
|-
| Builder + Auto Prover / models only
| [[#Cruise Control 0.5.0]]
| [[#Configuration 1]]
| 351.5 s (1550 / 2911 POs)
| 641.9 s (1550 / 2911 POs)
| 484.5 s (1574 / 2911 POs)
|-
|-
| Builder / models + proofs
| Builder / models + proofs
Line 102: Line 181:
| 108.6 s
| 108.6 s
| 199.1 s
| 199.1 s
| 125.9 s
| 123.3 s
|-
|-
| Builder / models only
| Builder / models only
Line 109: Line 188:
| 2060 ms
| 2060 ms
| 2524 ms
| 2524 ms
| 882 ms
| 995 ms
|-
| Builder + Auto Prover / models only
| [[#Cars on a Bridge]]
| [[#Configuration 1]]
| 4388 ms (237 / 237 POs)
| 4320 ms (237 / 237 POs)
| 3466 ms (237 / 237 POs)
|-
|-
| Builder / models + proofs
| Builder / models + proofs
Line 116: Line 202:
| 2843 ms
| 2843 ms
| 3360 ms
| 3360 ms
| 2018 ms
| 2238 ms
|-
|-
| Builder / models only
| Builder / models only
Line 123: Line 209:
|  
|  
| 88.7 s
| 88.7 s
| 9.3 s
| 11.2 s
|-
| Builder + Auto Prover / models only
| [[#Systerel Project]]
| [[#Configuration 1]]
|
| 185.7 s (1218 / 1360 POs)
| 162.3 s (1218 / 1360 POs)
|-
|-
| Builder / models + proofs
| Builder / models + proofs
Line 130: Line 223:
|  
|  
| 149.9 s
| 149.9 s
| 108.8 s
| 109.4 s
|}
|}
{| class="wikitable" style="text-align:center; width:80%;"
|+ Measures
|-
! scope=col | Test
! scope=col | Applied to
! scope=col | Configuration
! scope=col | Rodin 1.3
! scope=col | Rodin 2.0
! scope=col | Rodin 2.1
! scope=col | Rodin 2.2
|-
| Lexer
|
| [[#Configuration 2]]
| 18.2 s
| 21.8 s
| 33.7 s
| 30.7 s
|-
| Parser
|
| [[#Configuration 2]]
| 17.9 s
| 38.9 s
| 16.9 s
| 11.1 s
|-
| Builder / models only
| [[#Cruise Control 0.5.0]]
| [[#Configuration 2]]
| 124.2 s
| 206.7 s
| 32.5 s
| 33.1 s
|-
| Builder + Auto Prover / models only
| [[#Cruise Control 0.5.0]]
| [[#Configuration 2]]
| 356.7 s (1550 / 2911 POs)
| 633.4 s (1550 / 2911 POs)
| 505.5 s (1574 / 2911 POs)
| 477.2 s (1574 / 2911 POs)
|-
| Builder / models + proofs
| [[#Cruise Control 0.5.0]]
| [[#Configuration 2]]
| 120.7 s
| 204.9 s
| 126.5 s
| 111.9 s
|-
| Builder / models only
| [[#Cars on a Bridge]]
| [[#Configuration 2]]
| 1913 ms
| 2401 ms
| 839 ms
| 855 ms
|-
| Builder + Auto Prover / models only
| [[#Cars on a Bridge]]
| [[#Configuration 2]]
| 3934 ms (237 / 237 POs)
| 3888 ms (237 / 237 POs)
| 3413 ms (237 / 237 POs)
| 2536 ms (237 / 237 POs)
|-
| Builder / models + proofs
| [[#Cars on a Bridge]]
| [[#Configuration 2]]
| 2688 ms
| 3287 ms
| 2050 ms
| 1982 ms
|-
| Builder / models only
| [[#Systerel Project]]
| [[#Configuration 2]]
|
| 89.7 s
| 9.8 s
| 10.1 s
|-
| Builder + Auto Prover / models only
| [[#Systerel Project]]
| [[#Configuration 2]]
|
| 185.8 s (1218 / 1360 POs)
| 167.2 s (1218 / 1360 POs)
| 165.9 s (1218 / 1360 POs)
|-
| Builder / models + proofs
| [[#Systerel Project]]
| [[#Configuration 2]]
|
| 147.0 s
| 106.9 s
| 82.3 s
|-
| Builder / models only
| [[#XCore]]
| [[#Configuration 2]]
|
| 195.6 s
| 49.1 s
| 53.1 s
|-
| Builder + Auto Prover / models only
| [[#XCore]]
| [[#Configuration 2]]
|
| 377.7 s (2381 / 2595 POs)
| 271.6 s (2381 / 2595 POs)
| 308.8 s (2381 / 2595 POs)
|-
| Builder / models + proofs
| [[#XCore]]
| [[#Configuration 2]]
|
| 231.2 s
| 148.0 s
| 141.0 s
|-
| Builder / models only
| [[#XCore Encoding]]
| [[#Configuration 2]]
|
| 210.0 s
| 54.1 s
| 56.2 s
|-
| Builder + Auto Prover / models only
| [[#XCore Encoding]]
| [[#Configuration 2]]
|
| 367.3 s (1209 / 1370 POs)
| 243.5 s (1209 / 1370 POs)
| 262.3 s (1209 / 1370 POs)
|-
| Builder / models + proofs
| [[#XCore Encoding]]
| [[#Configuration 2]]
|
| 230.9 s
| 146.6 s
| 150.4 s
|}
The figure below presents and sums up the values of the table above:
[[Image:Rodin_Performances_Core_perf_fullv3.png|750px|center]]


Test Builder = SC + POG + POM, no proof attempt is performed.
Test Builder = SC + POG + POM, no proof attempt is performed.
[[Category:Rodin Platform Release Notes]]

Latest revision as of 08:43, 17 June 2011

Performance measures for the Rodin Platform.

Configurations

Configuration 1

System:

  • Intel Pentium Dual Core E2180 (2* 2 GHz)
  • 2 Go RAM

OS:

  • Ubuntu 10.10
  • linux kernel 2.6.35-25
  • GNOME 2.32.0

Java:

  • Java(TM) SE Runtime Environment (build 1.6.0_22-b04)
  • Java HotSpot(TM) Server VM (build 17.1-b03, mixed mode)
  • VM arguments
    • -Xms40m
    • -Xmx1200m

Eclipse:

  • Helios (3.6.1)
  • JUnit 4.8.1

Configuration 2

System:

  • Intel Pentium Dual Core E2180 (2* 2 GHz)
  • 2 Go RAM

OS:

  • Ubuntu 11.04
  • linux kernel 2.6.38-9
  • GNOME 2.32.1

Java:

  • Java(TM) SE Runtime Environment (build 1.6.0_24-b07)
  • Java HotSpot(TM) Server VM (build 19.1-b02, mixed mode)
  • VM arguments
    • -Xms40m
    • -Xmx1200m

Eclipse:

  • Helios (3.6.2)
  • JUnit 4.8.1


Benchmark Projects

Cruise Control 0.5.0

  • 7 Contexts
  • 49 Machines
  • 2911 POs

Cars on a Bridge

Taken from Jean-Raymond Abrial's book "Modeling in Event-B"

  • 3 Contexts
  • 4 Machines
  • 237 POs

Systerel Project

  • 9 Contexts
  • 14 Machines
  • 927 POs

XCore

  • 62 Contexts
  • 50 Machines
  • 2595 POs

XCore Encoding

  • 45 Contexts
  • 15 Machines
  • 1370 POs

Protocol

A measurement is launched using the JUnit plug-in fr.systerel.perf.tests. Tests are run from a freshly launched eclipse as only running user application, in UI thread, with an empty workbench.

Launch Configuration must include exactly the following plug-ins:

  • fr.systerel.perf.tests
  • org.eventb.core
  • org.eventb.core.seqprover
  • org.eventb.core.ast
  • org.rodinp.core

Every measurement starts with the build of a fake project intended to load all needed classes (extra time of more than 10 seconds has been observed for build). Class loading is intended to be optimised separately.

Verify that 1200 Mo are free when tests are ready for launch.

Tests

Lexer

A base string is made of all standard Event-B Mathematical Language symbols, separated from each other with a space character.

The string to lex is made of the concatenation of 100000 times the base string.

The lexer is called 10 times on the string to lex.

Parser

The parser is called on formulae covering all Event-B operators:

  • 43 predicates
  • 140 expressions
  • 7 assignments
  • 1 big predicate (1750 characters)

The parsing is repeated 4000 times.

Builder / models only

The project initially contains only model files (contexts and machines). It is built with auto provers turned off.

Builder + Auto Prover / models only

The project initially contains only model files (contexts and machines). It is built with auto provers turned on.

Builder / models + proofs

The project initially contains models and proofs (contexts, machines, proofs). It is built with auto provers turned off.


Results

The following results are means of 3 successive measures.

Measures
Test Applied to Configuration Rodin 1.3 Rodin 2.0 Rodin 2.1
Lexer #Configuration 1 19.0 s 21.4 s 35.6 s
Parser #Configuration 1 17.1 s 39.3 s 17.2 s
Builder / models only #Cruise Control 0.5.0 #Configuration 1 119.6 s 211.0 s 30.9 s
Builder + Auto Prover / models only #Cruise Control 0.5.0 #Configuration 1 351.5 s (1550 / 2911 POs) 641.9 s (1550 / 2911 POs) 484.5 s (1574 / 2911 POs)
Builder / models + proofs #Cruise Control 0.5.0 #Configuration 1 108.6 s 199.1 s 123.3 s
Builder / models only #Cars on a Bridge #Configuration 1 2060 ms 2524 ms 995 ms
Builder + Auto Prover / models only #Cars on a Bridge #Configuration 1 4388 ms (237 / 237 POs) 4320 ms (237 / 237 POs) 3466 ms (237 / 237 POs)
Builder / models + proofs #Cars on a Bridge #Configuration 1 2843 ms 3360 ms 2238 ms
Builder / models only #Systerel Project #Configuration 1 88.7 s 11.2 s
Builder + Auto Prover / models only #Systerel Project #Configuration 1 185.7 s (1218 / 1360 POs) 162.3 s (1218 / 1360 POs)
Builder / models + proofs #Systerel Project #Configuration 1 149.9 s 109.4 s
Measures
Test Applied to Configuration Rodin 1.3 Rodin 2.0 Rodin 2.1 Rodin 2.2
Lexer #Configuration 2 18.2 s 21.8 s 33.7 s 30.7 s
Parser #Configuration 2 17.9 s 38.9 s 16.9 s 11.1 s
Builder / models only #Cruise Control 0.5.0 #Configuration 2 124.2 s 206.7 s 32.5 s 33.1 s
Builder + Auto Prover / models only #Cruise Control 0.5.0 #Configuration 2 356.7 s (1550 / 2911 POs) 633.4 s (1550 / 2911 POs) 505.5 s (1574 / 2911 POs) 477.2 s (1574 / 2911 POs)
Builder / models + proofs #Cruise Control 0.5.0 #Configuration 2 120.7 s 204.9 s 126.5 s 111.9 s
Builder / models only #Cars on a Bridge #Configuration 2 1913 ms 2401 ms 839 ms 855 ms
Builder + Auto Prover / models only #Cars on a Bridge #Configuration 2 3934 ms (237 / 237 POs) 3888 ms (237 / 237 POs) 3413 ms (237 / 237 POs) 2536 ms (237 / 237 POs)
Builder / models + proofs #Cars on a Bridge #Configuration 2 2688 ms 3287 ms 2050 ms 1982 ms
Builder / models only #Systerel Project #Configuration 2 89.7 s 9.8 s 10.1 s
Builder + Auto Prover / models only #Systerel Project #Configuration 2 185.8 s (1218 / 1360 POs) 167.2 s (1218 / 1360 POs) 165.9 s (1218 / 1360 POs)
Builder / models + proofs #Systerel Project #Configuration 2 147.0 s 106.9 s 82.3 s
Builder / models only #XCore #Configuration 2 195.6 s 49.1 s 53.1 s
Builder + Auto Prover / models only #XCore #Configuration 2 377.7 s (2381 / 2595 POs) 271.6 s (2381 / 2595 POs) 308.8 s (2381 / 2595 POs)
Builder / models + proofs #XCore #Configuration 2 231.2 s 148.0 s 141.0 s
Builder / models only #XCore Encoding #Configuration 2 210.0 s 54.1 s 56.2 s
Builder + Auto Prover / models only #XCore Encoding #Configuration 2 367.3 s (1209 / 1370 POs) 243.5 s (1209 / 1370 POs) 262.3 s (1209 / 1370 POs)
Builder / models + proofs #XCore Encoding #Configuration 2 230.9 s 146.6 s 150.4 s


The figure below presents and sums up the values of the table above:

Test Builder = SC + POG + POM, no proof attempt is performed.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Performances&oldid=7290’