Rodin Performances: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Nicolas m →Results: fixed PO numbers |
imported>Nicolas m →Results: added results for 1.3 and 2.0 / config 2 |
||
| Line 240: | Line 240: | ||
| | | | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | 18.2 s | ||
| | | 21.8 s | ||
| | | 33.7 s | ||
| | | 30.9 s | ||
|- | |- | ||
| Parser | | Parser | ||
| | | | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | 17.9 s | ||
| | | 38.9 s | ||
| | | 16.9 s | ||
| | | 11.2 s | ||
|- | |- | ||
| Builder / models only | | Builder / models only | ||
| [[#Cruise Control 0.5.0]] | | [[#Cruise Control 0.5.0]] | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | 124.2 s | ||
| | | 206.7 s | ||
| s | | s | ||
| s | | s | ||
| Line 264: | Line 264: | ||
| [[#Cruise Control 0.5.0]] | | [[#Cruise Control 0.5.0]] | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | 356.7 s (1550 / 2911 POs) | ||
| | | 633.4 s (1550 / 2911 POs) | ||
| s ( / 2911 POs) | | s ( / 2911 POs) | ||
| s | | s | ||
| Line 272: | Line 272: | ||
| [[#Cruise Control 0.5.0]] | | [[#Cruise Control 0.5.0]] | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | 120.7 s | ||
| | | 204.9 s | ||
| s | | s | ||
| s | | s | ||
| Line 281: | Line 281: | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | | ||
| | | 89.7 s | ||
| s | | s | ||
| s | | s | ||
| Line 289: | Line 289: | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | | ||
| | | 185.8 s (1218 / 1360 POs) | ||
| s ( / 1360 POs) | | s ( / 1360 POs) | ||
| s | | s | ||
| Line 297: | Line 297: | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | | ||
| | | 147.0 s | ||
| s | | s | ||
| s | | s | ||
| Line 304: | Line 304: | ||
| [[#Cars on a Bridge]] | | [[#Cars on a Bridge]] | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | 1913 ms | ||
| | | 2401 ms | ||
| ms | | ms | ||
| ms | | ms | ||
| Line 312: | Line 312: | ||
| [[#Cars on a Bridge]] | | [[#Cars on a Bridge]] | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | 3934 ms (237 / 237 POs) | ||
| | | 3888 ms (237 / 237 POs) | ||
| ms (237 / 237 POs) | | ms (237 / 237 POs) | ||
| ms | | ms | ||
| Line 320: | Line 320: | ||
| [[#Cars on a Bridge]] | | [[#Cars on a Bridge]] | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | 2688 ms | ||
| | | 3287 ms | ||
| ms | | ms | ||
| ms | | ms | ||
| Line 329: | Line 329: | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | | ||
| | | 195.6 s | ||
| s | | s | ||
| s | | s | ||
| Line 337: | Line 337: | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | | ||
| | | 377.7 s (2381 / 2595 POs) | ||
| s ( / 2595 POs) | | s ( / 2595 POs) | ||
| s ( / 2595 POs) | | s ( / 2595 POs) | ||
| Line 345: | Line 345: | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | | ||
| | | 231.2 s | ||
| s | | s | ||
| s | | s | ||
| Line 353: | Line 353: | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | | ||
| | | 210.0 s | ||
| s | | s | ||
| s | | s | ||
| Line 361: | Line 361: | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | | ||
| | | 367.3 s (1209 / 1370 POs) | ||
| s ( / 1370 POs) | | s ( / 1370 POs) | ||
| s ( / 1370 POs) | | s ( / 1370 POs) | ||
| Line 369: | Line 369: | ||
| [[#Configuration 2]] | | [[#Configuration 2]] | ||
| | | | ||
| | | 230.9 s | ||
| s | | s | ||
| s | | s | ||
Revision as of 21:34, 19 May 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.
| 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 |
| 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.9 s | |
| Parser | #Configuration 2 | 17.9 s | 38.9 s | 16.9 s | 11.2 s | |
| Builder / models only | #Cruise Control 0.5.0 | #Configuration 2 | 124.2 s | 206.7 s | s | 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) | s ( / 2911 POs) | s |
| Builder / models + proofs | #Cruise Control 0.5.0 | #Configuration 2 | 120.7 s | 204.9 s | s | s |
| Builder / models only | #Systerel Project | #Configuration 2 | 89.7 s | s | s | |
| Builder + Auto Prover / models only | #Systerel Project | #Configuration 2 | 185.8 s (1218 / 1360 POs) | s ( / 1360 POs) | s | |
| Builder / models + proofs | #Systerel Project | #Configuration 2 | 147.0 s | s | s | |
| Builder / models only | #Cars on a Bridge | #Configuration 2 | 1913 ms | 2401 ms | ms | ms |
| Builder + Auto Prover / models only | #Cars on a Bridge | #Configuration 2 | 3934 ms (237 / 237 POs) | 3888 ms (237 / 237 POs) | ms (237 / 237 POs) | ms |
| Builder / models + proofs | #Cars on a Bridge | #Configuration 2 | 2688 ms | 3287 ms | ms | ms |
| Builder / models only | #XCore | #Configuration 2 | 195.6 s | s | s | |
| Builder + Auto Prover / models only | #XCore | #Configuration 2 | 377.7 s (2381 / 2595 POs) | s ( / 2595 POs) | s ( / 2595 POs) | |
| Builder / models + proofs | #XCore | #Configuration 2 | 231.2 s | s | s | |
| Builder / models only | #XCore Encoding | #Configuration 2 | 210.0 s | s | s | |
| Builder + Auto Prover / models only | #XCore Encoding | #Configuration 2 | 367.3 s (1209 / 1370 POs) | s ( / 1370 POs) | s ( / 1370 POs) | |
| Builder / models + proofs | #XCore Encoding | #Configuration 2 | 230.9 s | s | s |
The figure below presents and sums up the values of the table above:
Test Builder = SC + POG + POM, no proof attempt is performed.
