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>Tommy
Line 132: Line 132:
| 108.8 s
| 108.8 s
|}
|}
The figure below presents and sums up the values of the table above:
[[Image:Rodin_Performances_core_perf_full.png|750px|center]]


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

Revision as of 18:31, 1 February 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-24
  • 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
  • tests run from a freshly launched eclipse as only running user application, in UI thread, with an empty workbench.

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

Protocol

A measurement is launched using the JUnit plug-in fr.systerel.perf.tests.

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.

Results

Measures
Test Applied to Configuration Rodin 1.3 Rodin 2.0 Rodin 2.1 (temporary results)
Lexer #Configuration 1 19.0 s 21.4 s 34.9 s
Parser #Configuration 1 17.1 s 39.3 s 17.1 s
Builder / models only #Cruise Control 0.5.0 #Configuration 1 119.6 s 211.0 s 32.3 s
Builder / models + proofs #Cruise Control 0.5.0 #Configuration 1 108.6 s 199.1 s 125.9 s
Builder / models only #Cars on a Bridge #Configuration 1 2060 ms 2524 ms 882 ms
Builder / models + proofs #Cars on a Bridge #Configuration 1 2843 ms 3360 ms 2018 ms
Builder / models only #Systerel Project #Configuration 1 88.7 s 9.3 s
Builder / models + proofs #Systerel Project #Configuration 1 149.9 s 108.8 s


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

File:Rodin Performances core perf full.png

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