Rodin Performances: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Tommy |
imported>Nicolas |
||
| Line 74: | Line 74: | ||
! 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 | ! scope=col | Rodin 2.1 | ||
|- | |- | ||
| Lexer | | Lexer | ||
| Line 81: | Line 81: | ||
| 19.0 s | | 19.0 s | ||
| 21.4 s | | 21.4 s | ||
| | | 35.6 s | ||
|- | |- | ||
| Parser | | Parser | ||
| Line 88: | Line 88: | ||
| 17.1 s | | 17.1 s | ||
| 39.3 s | | 39.3 s | ||
| 17. | | 17.2 s | ||
|- | |- | ||
| Builder / models only | | Builder / models only | ||
| Line 95: | Line 95: | ||
| 119.6 s | | 119.6 s | ||
| 211.0 s | | 211.0 s | ||
| | | 30.9 s | ||
|- | |- | ||
| Builder / models + proofs | | Builder / models + proofs | ||
| Line 102: | Line 102: | ||
| 108.6 s | | 108.6 s | ||
| 199.1 s | | 199.1 s | ||
| | | 123.3 s | ||
|- | |- | ||
| Builder / models only | | Builder / models only | ||
| Line 109: | Line 109: | ||
| 2060 ms | | 2060 ms | ||
| 2524 ms | | 2524 ms | ||
| | | 995 ms | ||
|- | |- | ||
| Builder / models + proofs | | Builder / models + proofs | ||
| Line 116: | Line 116: | ||
| 2843 ms | | 2843 ms | ||
| 3360 ms | | 3360 ms | ||
| | | 2238 ms | ||
|- | |- | ||
| Builder / models only | | Builder / models only | ||
| Line 123: | Line 123: | ||
| | | | ||
| 88.7 s | | 88.7 s | ||
| | | 11.2 s | ||
|- | |- | ||
| Builder / models + proofs | | Builder / models + proofs | ||
| Line 130: | Line 130: | ||
| | | | ||
| 149.9 s | | 149.9 s | ||
| | | 109.4 s | ||
|} | |} | ||
Revision as of 15:09, 2 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
| 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 / 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 / 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 / models + proofs | #Systerel Project | #Configuration 1 | 149.9 s | 109.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.
