Difference between pages "D45 Prover Enhancement" and "D45 Scalability"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
imported>Tommy
 
Line 1: Line 1:
 
= Overview =
 
= Overview =
* Two tasks concerned the prover performance from the core platform: the addition of rewriting and inference rules, and the addition of a mechanism to allow the customization and the parametrization or combination of tactics. While the addition of rewriting and inference rules has always been a regular task to enhance the Rodin integrated prover during DEPLOY lifetime, a new way to manage tactics has been implemented. In fact, the user is now able to define various types of tactics called 'profiles' which could be customized and parameterized tactics to discharge some specific proof obligations.
+
* '''Improved Performance''' According to the refocus mentionned in the [[D45_General_Platform_Maintenance#Motivations| General Platform Maintenance]] chapter, much of the reworking efforts performed on the core plateform basically aimed to overcome Rodin scalability weaknesses, and the continuous need of seamless proving experience. The whole performance was enhanced by core implementation and user interface refactorings. Improvements made to the proving experience will be detailed in a separate chapter.
* {{TODO}} An overview of the contribution about the ProB Disprover (Daniel Plagge, Jens Bendiposto)  
+
* {{TODO}} An overview of the contribution about the design pattern management / Generic Instantiation (Thai Son Hoang)  
* The SMT Solvers plug-in allowing to use the SMT solvers within Rodin is an effective alternative to the Atelier-B provers, particularly when reasoning on linear arithmetic. {{TODO}} (Laurent Voisin, Yoann Guyot)
+
* '''Edition''' It appeard, even more during the two last years of DEPLOY, the models defined by pilots becoming industrial sized due to the level of complexity reached, that the edition became a central concern.
  
 
= Motivations =
 
= Motivations =
== New rewriting and inference rules ==
 
In an Event-B development, more than 60% of the time is spent on proofs. It has been a continuous aim to increase the number of automatically discharged proof obligations (POs) by improving the capabilities of the integrated sequent prover through the addition of rewriting and inference rules. These rules were provided through tactics, or existing or newly created. These tactics were automatic, or manual, or sometimes both. Providing new proving rules, even if it sometimes does not increase directly the number of automatically discharged POs aims to help the user to interactively discharge them and spare his time.
 
  
== Advanced Preferences for Auto-tactics ==
+
== Improved Performance ==
{{TODO}} ''To be completed by Nicolas Beauger''
+
It appeared that the various DEPLOY partners encountered several major issues while editing large models. Some were related to the core code of the Rodin platform, causing crashes, loss of data, corruption in models. Some other were related to the UI causing platform hanging, and sometimes leading to its freezing which required sometimes to kill the Rodin process, thus also leading to potential loss of data and corruption in models. Hence, it appeared necessary to solve such issues before the end of DEPLOY.
Sometimes, the automatic proofs fail because the order of the applied tactics doesn't lead to the proof obligation discharge. Previously the ordering of tactics was lost at each change. Another issue is to have more than one possibility to combine the tactics. Indeed, various combinators called ''tacticals'' allow to combine tactics in a specific manner thus providing a sort of tactic arithmetic. The advanced preferences for auto-tactics solved this two issues.
 
  
== Isabelle Plug-in ==
+
== Design Pattern Management / Generic Instantiation  ==
{{TODO}} ''To be completed by Matthias Schmaltz''
+
{{TODO}} ''To be completed by Thai Son Hoang''
== ProB Disprover ==
+
== Edition ==
{{TODO}} ''Daniel Plagge, Jens Bendiposto''
+
{{TODO}} ''To be completed by Thomas Muller, Ingo Weigelt''
== SMT Solver Integration ==
 
{{TODO}} ''Laurent Voisin'' & ''Yoann Guyot''
 
  
 
= Choices / Decisions =
 
= Choices / Decisions =
== New rewriting and inference rules ==
+
== Improved Performance ==
{{TODO}} ''To be completed by Laurent Voisin''
+
SYSTEREL lead a two phase investigation to have a better idea of the work to be done. Each phase being followed by some refactoring of the code. Out of the early investigation, a cause and effect relationship has been found between perfomance loss and the various reported bugs, such as "platform hanging" bugs or even "no more handle" bugs related to the high consumption of graphical elements on Windows platforms. Indeed, it appeared that solving the performance issues sometimes solved induced bugs as well which made the scalability improvement tasks emcompass the maintenance goals.<br>
== Advanced Preferences for Auto-tactics ==
+
Later, a deeper investigation was performed, to indentify and tackle the remaining performance issues. Profiling and code review were the two techniques used. The profiling strategy allowed to get a better localisation of the performance loss in both UI and core code while the code review helped to understand the intrinsic misuses or drawbacks of particular components and/or architectures.
{{TODO}} ''To be completed by Nicolas Beauger''
+
A good example, was the Event-B built-in editor based on form editors with a high use of greedy graphical components. Such architecture appeard to be weak when it was needed to display industrial size models. This affected the modelling experience with some long, and really annoying to the user, reaction lags. To solve such issue, it has been chosen to refactor the editors using a textual representation which was a light-weight graphical alternative to lower the number of needed components.
Since Rodin 2.1, simple tactic profiles have been added. They allow to persiste and set specifically for some project various ordered ways to apply the basic tactics. Since Rodin 2.3, tacticals and parameterisation have been added to the profiles increasing even more the potential of such proving feature. The combinators allow for exemple to loop on a subset of tactics, including existing profiles, and the parameterisation allows for example to set a timeout on external provers such as AtelierB P1.
 
  
== Isabelle Plug-in ==
+
== Design Pattern Management / Generic Instantiation  ==
{{TODO}} ''To be completed by Matthias Schmaltz''
+
{{TODO}} ''To be completed by Thai Son Hoang''
== ProB Disprover ==
+
== Edition ==
{{TODO}} ''Daniel Plagge, Jens Bendiposto''
+
{{TODO}} ''To be completed by Thomas Muller, Ingo Weigelt''
== SMT Solver Integration ==
 
{{TODO}} ''Laurent Voisin'' & ''Yoann Guyot''
 
  
 
= Available Documentation =
 
= Available Documentation =
* {{TODO}} Links for New rewriting and inference rules
+
* {{TODO}} Links for Improved Performance
* {{TODO}} Links for Advanced Preferences for Auto-tactics
+
* {{TODO}} Links for Design Pattern Management / Generic Instantiation
* {{TODO}} Links for Isabelle Plug-in
+
* {{TODO}} Links for Edition
* {{TODO}} Links for ProB Disprover
 
* {{TODO}} Links for SMT Solver Integration
 
  
 
= Status =
 
= Status =
== New rewriting and inference rules ==
+
== Improved Performance ==
{{TODO}} ''To be completed by Laurent Voisin''
+
The refactoring made on both core code and UI code allowed to gain up to 25 times speed-up on the UI, and almost a 2 times speed-up in the core code, making the platform usable in an industrial sized context.<br>
== Advanced Preferences for Auto-tactics ==
+
 
{{TODO}} ''To be completed by Nicolas Beauger''
+
== Design Pattern Management / Generic Instantiation  ==
== Isabelle Plug-in ==
+
{{TODO}} ''To be completed by Thai Son Hoang''
{{TODO}} ''To be completed by Matthias Schmaltz''
+
== Edition ==
== ProB Disprover ==
+
{{TODO}} ''To be completed by Thomas Muller, Ingo Weigelt''
{{TODO}} ''Daniel Plagge, Jens Bendiposto''
 
== SMT Solver Integration ==
 
{{TODO}} ''Laurent Voisin'' & ''Yoann Guyot''
 
  
 
[[Category:D45 Deliverable]]
 
[[Category:D45 Deliverable]]

Revision as of 18:38, 18 November 2011

Overview

  • Improved Performance According to the refocus mentionned in the General Platform Maintenance chapter, much of the reworking efforts performed on the core plateform basically aimed to overcome Rodin scalability weaknesses, and the continuous need of seamless proving experience. The whole performance was enhanced by core implementation and user interface refactorings. Improvements made to the proving experience will be detailed in a separate chapter.
  • TODO An overview of the contribution about the design pattern management / Generic Instantiation (Thai Son Hoang)
  • Edition It appeard, even more during the two last years of DEPLOY, the models defined by pilots becoming industrial sized due to the level of complexity reached, that the edition became a central concern.

Motivations

Improved Performance

It appeared that the various DEPLOY partners encountered several major issues while editing large models. Some were related to the core code of the Rodin platform, causing crashes, loss of data, corruption in models. Some other were related to the UI causing platform hanging, and sometimes leading to its freezing which required sometimes to kill the Rodin process, thus also leading to potential loss of data and corruption in models. Hence, it appeared necessary to solve such issues before the end of DEPLOY.

Design Pattern Management / Generic Instantiation

TODO To be completed by Thai Son Hoang

Edition

TODO To be completed by Thomas Muller, Ingo Weigelt

Choices / Decisions

Improved Performance

SYSTEREL lead a two phase investigation to have a better idea of the work to be done. Each phase being followed by some refactoring of the code. Out of the early investigation, a cause and effect relationship has been found between perfomance loss and the various reported bugs, such as "platform hanging" bugs or even "no more handle" bugs related to the high consumption of graphical elements on Windows platforms. Indeed, it appeared that solving the performance issues sometimes solved induced bugs as well which made the scalability improvement tasks emcompass the maintenance goals.
Later, a deeper investigation was performed, to indentify and tackle the remaining performance issues. Profiling and code review were the two techniques used. The profiling strategy allowed to get a better localisation of the performance loss in both UI and core code while the code review helped to understand the intrinsic misuses or drawbacks of particular components and/or architectures. A good example, was the Event-B built-in editor based on form editors with a high use of greedy graphical components. Such architecture appeard to be weak when it was needed to display industrial size models. This affected the modelling experience with some long, and really annoying to the user, reaction lags. To solve such issue, it has been chosen to refactor the editors using a textual representation which was a light-weight graphical alternative to lower the number of needed components.

Design Pattern Management / Generic Instantiation

TODO To be completed by Thai Son Hoang

Edition

TODO To be completed by Thomas Muller, Ingo Weigelt

Available Documentation

  • TODO Links for Improved Performance
  • TODO Links for Design Pattern Management / Generic Instantiation
  • TODO Links for Edition

Status

Improved Performance

The refactoring made on both core code and UI code allowed to gain up to 25 times speed-up on the UI, and almost a 2 times speed-up in the core code, making the platform usable in an industrial sized context.

Design Pattern Management / Generic Instantiation

TODO To be completed by Thai Son Hoang

Edition

TODO To be completed by Thomas Muller, Ingo Weigelt