Tutorial Various Optimizations - Revision history

David Geleßus: Update PDF link

2021-02-04T17:11:46Z

Update PDF link

← Older revision		Revision as of 17:11, 4 February 2021
Line 30:		Line 30:
	[[File:partial_state_space_por.png]]		[[File:partial_state_space_por.png]]

	Using this observation the ordinary model checker of ProB has been extended to check a model formalized in B or Event-B using partial order reduction. More information about the implementation of POR in ProB and the theoretical background of POR can be read [~~http~~://~~www~~.~~stups.uni-duesseldorf~~.de/~~mediawiki/images~~/5/5b/~~Pub-~~DobrikovLeuschelPORtechreport.pdf here]. Our implementation of POR uses the ample set theory <ref>E.M. Clarke, O. Grumberg, M. Minea, and D. Peled: ''State Space Reduction using Partial Order Reduction''. STTT '98, 3, pages 279-287</ref>.		Using this observation the ordinary model checker of ProB has been extended to check a model formalized in B or Event-B using partial order reduction. More information about the implementation of POR in ProB and the theoretical background of POR can be read [https://www3.hhu.de/stups/downloads/pdf/DobrikovLeuschelPORtechreport.pdf here]. Our implementation of POR uses the ample set theory <ref>E.M. Clarke, O. Grumberg, M. Minea, and D. Peled: ''State Space Reduction using Partial Order Reduction''. STTT '98, 3, pages 279-287</ref>.

	For enabling the POR optimization for the model checker in Tcl/Tk interface of ProB a new check box “Partial Order Reduction” has been added to the “Model Checker” menu. Note that the option shows up only when the user mode is set to “Normal” (see Preferences → User Mode in the menu bar). The POR optimization can be enabled for model checking B and Event-B models with the command line version of ProB by setting the 'por' preference to the value 'ample_sets'. For example, the machine ''Example'' can be checked for deadlock and invariant violations using the POR optimization with the command line version of ProB as follows:		For enabling the POR optimization for the model checker in Tcl/Tk interface of ProB a new check box “Partial Order Reduction” has been added to the “Model Checker” menu. Note that the option shows up only when the user mode is set to “Normal” (see Preferences → User Mode in the menu bar). The POR optimization can be enabled for model checking B and Event-B models with the command line version of ProB by setting the 'por' preference to the value 'ample_sets'. For example, the machine ''Example'' can be checked for deadlock and invariant violations using the POR optimization with the command line version of ProB as follows:

Michael Leuschel at 16:58, 27 January 2021

2021-01-27T16:58:38Z

← Older revision		Revision as of 16:58, 27 January 2021
Line 94:		Line 94:
	To sum up, in order to take an advantage of POR the model being checked should have many independent operations that are concurrently executed. In other words, the magnitude of reduction depends on the coupling between the operations in the B model. Thus, it is recommended to use the reduced search when the analyzed model has comparatively many independent operations that are concurrently executed in order to gain from the improvement by the reduction technique. For example, if a B model has no pair of independent operations or all independent operations are not executed concurrently, i.e. two independent operations are never simultaneously enabled, then no reductions of the state space will be performed using the reduced search algorithm.		To sum up, in order to take an advantage of POR the model being checked should have many independent operations that are concurrently executed. In other words, the magnitude of reduction depends on the coupling between the operations in the B model. Thus, it is recommended to use the reduced search when the analyzed model has comparatively many independent operations that are concurrently executed in order to gain from the improvement by the reduction technique. For example, if a B model has no pair of independent operations or all independent operations are not executed concurrently, i.e. two independent operations are never simultaneously enabled, then no reductions of the state space will be performed using the reduced search algorithm.

	The reduction algorithm has been evaluated on various B and Event-B models. The evaluation can be obtained [~~http~~://~~nightly~~.~~cobra.cs.uni-duesseldorf~~.de/por/ here].		The reduction algorithm has been evaluated on various B and Event-B models. The evaluation can be obtained [https://www3.hhu.de/stups/internal/benchmarks/por/ here].

	== Partial Guard Evaluation ==		== Partial Guard Evaluation ==
Line 255:		Line 255:
	In all test cases except for 'All Enabled' and 'Cruise Control' model checking with PGE has provided better performance results than model checking without PGE. The results show that partial guard evaluation can improve model checking up to factor 2. The larger the state space the higher is the possibility for better performance in model checking B models. For example, for 'CAN BUS' the optimisation could speed up model checking to factor 2, whereas for the 'Crusie Control' model no improvement could be detected although a significant number of guard evaluations could be saved up.		In all test cases except for 'All Enabled' and 'Cruise Control' model checking with PGE has provided better performance results than model checking without PGE. The results show that partial guard evaluation can improve model checking up to factor 2. The larger the state space the higher is the possibility for better performance in model checking B models. For example, for 'CAN BUS' the optimisation could speed up model checking to factor 2, whereas for the 'Crusie Control' model no improvement could be detected although a significant number of guard evaluations could be saved up.

	These and various other benchmarks used for evaluating partial guard evaluation (PGE) can be viewed [~~http~~://~~nightly~~.~~cobra.cs.uni-duesseldorf~~.de/pge/ here].		These and various other benchmarks used for evaluating partial guard evaluation (PGE) can be viewed [https://www3.hhu.de/stups/internal/benchmarks/pge/ here].

	== References ==		== References ==
	<references />		<references />

Ivaylo Dobrikov: /* Partial Guard Evaluation */

2016-02-02T16:11:00Z

Partial Guard Evaluation

← Older revision		Revision as of 16:11, 2 February 2016
Line 103:		Line 103:
	# Applying the machine's operations to <tt>s</tt>.		# Applying the machine's operations to <tt>s</tt>.

	The second step is carried out in case no error was discovered previously (in step 1.). When step 2. is performed in some state <tt>s</tt> all operations of the checked B model are tested for being enabled in <tt>s</tt> and the substitutions of each enabled operation are performed at <tt>s</tt>.		The second step is carried out in case no error was discovered previously (in step 1). When step 2. is performed in some state <tt>s</tt> all operations of the checked B model are tested for being enabled in <tt>s</tt> and the substitutions of each enabled operation are performed at <tt>s</tt>.

	The effort of checking a state amounts thus to checking the state for errors (testing for invariant violation, assertion violations etc.) plus the computation of the successors. There is some redundancy in testing all operations' guards in each state, as usually there are operations that are disabled in the states being explored. Especially, when the model checker has to check exhaustively B models with large state spaces the effort of testing the guard of each operation in every state may be huge. Thus, an optimization may be considered by means of decreasing the state space exploration complexity by trying to reduce the overall number of guard tests via skipping the guard evaluations of operations known to be disabled in some states.		The effort of checking a state amounts thus to checking the state for errors (testing for invariant violation, assertion violations etc.) plus the computation of the successors. There is some redundancy in testing all operations' guards in each state, as usually there are operations that are disabled in the states being explored. Especially, when the model checker has to check exhaustively B models with large state spaces the effort of testing the guard of each operation in every state may be huge. Thus, an optimization may be considered by means of decreasing the state space exploration complexity by trying to reduce the overall number of guard tests via skipping the guard evaluations of operations known to be disabled in some states.

Ivaylo Dobrikov: /* Partial Order Reduction */

2016-01-29T15:05:57Z

Partial Order Reduction

← Older revision		Revision as of 15:05, 29 January 2016
Line 26:		Line 26:
	[[File:full_state_space_por.png]]		[[File:full_state_space_por.png]]

	Since the order in which the operations are executed is not relevant for discovering the deadlock state it is sufficient to examine only one of the six paths that start in the initial state and reach the deadlock. Thus, for the machine it is enough to analyze only one arbitrary order of the events in order to detect the deadlock:		Since the order in which the operations are executed is not relevant for discovering the deadlock state it is sufficient to examine only one of the six possible paths that start in the initial state and reach the deadlock. Thus, for the machine it is enough to analyze only one arbitrary order of the events in order to detect the deadlock:

	[[File:partial_state_space_por.png]]		[[File:partial_state_space_por.png]]

Ivaylo Dobrikov at 13:30, 29 January 2016

2016-01-29T13:30:44Z

← Older revision		Revision as of 13:30, 29 January 2016
Line 151:		Line 151:
	In the B machine the operations `Req1`, `Enter1` and `Rel1` represent the actions ''request'', ''enter'' and ''release'' of <math>P_1</math>, respectively. Analogously, the operations `Req2`, `Enter2` and `Rel2` represent the actions ''request'', ''enter'' and ''release'' of <math>P_2</math>, respectively. The requirement ''always at most one process is in its critical section'' guaranteeing the mutual exclusion property is stated in the invariant of the machine by means of the predicate <tt> not(p1 = crit1 & p2 = crit2)</tt>.		In the B machine the operations `Req1`, `Enter1` and `Rel1` represent the actions ''request'', ''enter'' and ''release'' of <math>P_1</math>, respectively. Analogously, the operations `Req2`, `Enter2` and `Rel2` represent the actions ''request'', ''enter'' and ''release'' of <math>P_2</math>, respectively. The requirement ''always at most one process is in its critical section'' guaranteeing the mutual exclusion property is stated in the invariant of the machine by means of the predicate <tt> not(p1 = crit1 & p2 = crit2)</tt>.

	To verify that the B machine satisfy the mutual exclusion property and has no deadlock state one can use the ProB model checker. This will explicitly generate all possible states of the machine and check whether there is any state that is a deadlock state or that violates the invariant. As a result, 8 states will be generated and checked, the machine is consistent with respect to the invariant and has no deadlock state. By the exhaustive search for error states the model checker will test by exploring the state space each guard of the machine’s operations for being ~~enabling~~ in the currently processed state. That is, while exploring the state space of the machine 48 guard tests (8 states <math>\times</math> 6 operations) will be performed in order to ~~explore~~ the entire state space.		To verify that the B machine satisfy the mutual exclusion property and has no deadlock state one can use the ProB model checker. This will explicitly generate all possible states of the machine and check whether there is any state that is a deadlock state or that violates the invariant. As a result, 8 states will be generated and checked, the machine is consistent with respect to the invariant and has no deadlock state. By the exhaustive search for error states the model checker will test by exploring the state space each guard of the machine’s operations for being enabled in the currently processed state. That is, while exploring the state space of the machine 48 guard tests (8 states <math>\times</math> 6 operations) will be performed in order to unfold the entire state space of the MutualExclusion machine.

	[[File:StateSpacePGE.png]]		[[File:StateSpacePGE.png]]

Ivaylo Dobrikov: /* Partial Guard Evaluation */

2016-01-29T13:02:43Z

Partial Guard Evaluation

← Older revision		Revision as of 13:02, 29 January 2016
Line 125:		Line 125:
	* [[file: KeepRelation.png]]<br/><tt>Op1</tt> '''keeps''' <tt>Op2</tt> enabled respectively disabled		* [[file: KeepRelation.png]]<br/><tt>Op1</tt> '''keeps''' <tt>Op2</tt> enabled respectively disabled

	Consider the B machine below modelling an algorithm for mutual exclusion with a semaphore (variable <tt>y</tt> ~~in the machine below~~) for two concurrent processes <math>P_1</math> and <math>P_2</math>. Each process has been simplified to perform three types of actions: ''request'' (for entering in the critical section), ''enter'' (entering the critical section), and ''release'' (exiting the critical section).		Consider the B machine below modelling an algorithm for mutual exclusion with a semaphore (in the machine below this is variable <tt>y</tt>) for two concurrent processes <math>P_1</math> and <math>P_2</math>. Each process has been simplified to perform three types of actions: ''request'' (for entering in the critical section), ''enter'' (entering the critical section), and ''release'' (exiting the critical section).

	<pre>		<pre>

Ivaylo Dobrikov at 11:22, 29 January 2016

2016-01-29T11:22:05Z

← Older revision		Revision as of 11:22, 29 January 2016
Line 125:		Line 125:
	* [[file: KeepRelation.png]]<br/><tt>Op1</tt> '''keeps''' <tt>Op2</tt> enabled respectively disabled		* [[file: KeepRelation.png]]<br/><tt>Op1</tt> '''keeps''' <tt>Op2</tt> enabled respectively disabled

	Consider the B machine below modelling an algorithm for mutual exclusion with ~~semaphores~~ for two concurrent processes<math>P_1</math> and <math>P_2</math>. Each process has been simplified to perform three types of actions: ''request'' (for entering in the critical section), ''enter'' (entering the critical section), and ''release'' (exiting the critical section).		Consider the B machine below modelling an algorithm for mutual exclusion with a semaphore (variable <tt>y</tt> in the machine below) for two concurrent processes <math>P_1</math> and <math>P_2</math>. Each process has been simplified to perform three types of actions: ''request'' (for entering in the critical section), ''enter'' (entering the critical section), and ''release'' (exiting the critical section).

	<pre>		<pre>

Ivaylo Dobrikov: /* Partial Guard Evaluation */

2016-01-29T11:15:58Z

Partial Guard Evaluation

← Older revision		Revision as of 11:15, 29 January 2016
Line 123:		Line 123:
	*[[file: GuaranteedRelation.png]] <br/><tt>Op2</tt> is '''always''' enabled after the execution of <tt>Op1</tt>		*[[file: GuaranteedRelation.png]] <br/><tt>Op2</tt> is '''always''' enabled after the execution of <tt>Op1</tt>
	*[[file: ImpossibleRelation.png]] <br/><tt>Op2</tt> is '''impossible''' to be enabled after the execution of <tt>Op1</tt>		*[[file: ImpossibleRelation.png]] <br/><tt>Op2</tt> is '''impossible''' to be enabled after the execution of <tt>Op1</tt>
	* [[file: KeepRelation.png]]<br/><tt>~~Op2~~</tt> '''keeps''' <tt>~~Op1~~</tt> enabled respectively disabled		* [[file: KeepRelation.png]]<br/><tt>Op1</tt> '''keeps''' <tt>Op2</tt> enabled respectively disabled

	Consider the B machine below modelling an algorithm for mutual exclusion with semaphores for two concurrent processes<math>P_1</math> and <math>P_2</math>. Each process has been simplified to perform three types of actions: ''request'' (for entering in the critical section), ''enter'' (entering the critical section), and ''release'' (exiting the critical section).		Consider the B machine below modelling an algorithm for mutual exclusion with semaphores for two concurrent processes<math>P_1</math> and <math>P_2</math>. Each process has been simplified to perform three types of actions: ''request'' (for entering in the critical section), ''enter'' (entering the critical section), and ''release'' (exiting the critical section).

Ivaylo Dobrikov: /* Partial Guard Evaluation */

2015-09-07T09:14:19Z

Partial Guard Evaluation

← Older revision		Revision as of 09:14, 7 September 2015
Line 219:		Line 219:


	Let us now consider state <math>s_2</math> in Figure 1 that we assume to be yet ~~non-~~explored by the model checker. <math>s_2</math> is an after-state of `Req1`. Using the enabling relations that we have established we can infer that `Req1` and `Rel1` are disabled at <math>s_2</math> since both are impossible to be enabled in each after-state of `Req1`. Further, we can ~~spare~~ the ~~test~~ of the guards of `Enter2` and `Rel2` since both operations are disabled in <math>s_1</math> and we already have shown that `Req1` cannot change the status of the guard of both operations. As a result, we can skip the test for enabledness for `Req1`, `Rel1`, `Enter2` and `Rel2` in <math>s_2</math>. The test of the guard of `Req2` can also be omitted since `Req2` is enabled in <math>s_1</math> and thus also enabled in <math>s_2</math> as `Req1` keeps `Req2` enabled. Summarizing these results, it is thus necessary to test only the guard of `Enter1` in <math>s_2</math> as we could determine the status of the guards of the residual operations via the enabling relations that we considered previously.		Let us now consider state <math>s_2</math> in Figure 1 that we assume to be yet not explored by the model checker. <math>s_2</math> is an after-state of `Req1`. Using the enabling relations that we have established we can infer that `Req1` and `Rel1` are disabled at <math>s_2</math> since both are impossible to be enabled in each after-state of `Req1`. Further, we can omit the tests of the guards of `Enter2` and `Rel2` since both operations are disabled in <math>s_1</math> and we already have shown that `Req1` cannot change the status of the guard of both operations. As a result, we can skip the test for enabledness for `Req1`, `Rel1`, `Enter2` and `Rel2` in <math>s_2</math>. The test of the guard of `Req2` can also be omitted since `Req2` is enabled in <math>s_1</math> and thus also enabled in <math>s_2</math> as `Req1` keeps `Req2` enabled. Summarizing these results, it is thus necessary to test only the guard of `Enter1` in <math>s_2</math> as we could determine the status of the guards of the residual operations via the enabling relations that we considered previously.

	Partial guard evaluation (PGE) makes use of the enabling relations. Above we described how guard tests can be saved up aiming to optimise the exploration of the state space and thus to provide smaller model checking times for B models, as well as for Event-B models. The optimisation can be enabled using the preference ('-p') option in case the command line of the ProB tool is used for model checking:		Partial guard evaluation (PGE) makes use of the enabling relations. Above we described how guard tests can be saved up aiming to optimise the exploration of the state space and thus to provide smaller model checking times for B models, as well as for Event-B models. The optimisation can be enabled using the preference ('-p') option in case the command line of the ProB tool is used for model checking:
Line 243:		Line 243:
	[[ file: StateSpaceDepthFirst.png ]]		[[ file: StateSpaceDepthFirst.png ]]

	Let us consider the explored state space in Figure 3. Using breadth-first search will explore all states above <math>s_7</math> and <math>s_8</math> until <math>s_7</math> is reached. When <math>s_7</math> is explored the operation `Enter1` will also be considered in the course of analysing which operations are disabled and enabled at <math>s_7</math> as in the figure below state <math>s_5</math> was already explored and `Enter1` is an incoming transition of <math>s_7</math>. Using the results from the table above, we can infer that `Enter2` is disabled at <math>s_7</math> since it is impossible for `Enter2`to be enabled after the execution of `Enter1`. If we use the results inferred by analysing the enabling relation in regard to `Req2`, then we can conclude that all operations are disabled in <math>s_7</math> except for `Rel1`. Thus, in this case we saved up one guard test more in comparison to the depth-first search example.		Let us now consider the explored state space in Figure 3. Using breadth-first search will explore all states above <math>s_7</math> and <math>s_8</math> until <math>s_7</math> is reached. When <math>s_7</math> is explored the operation `Enter1` will also be considered in the course of analysing which operations are disabled and enabled at <math>s_7</math> as in the figure below state <math>s_5</math> was already explored and `Enter1` is an incoming transition of <math>s_7</math>. Using the results from the table above, we can infer that `Enter2` is disabled at <math>s_7</math> since it is impossible for `Enter2`to be enabled after the execution of `Enter1` (see the Enabling Analysis table above). If we use the results inferred by analysing the enabling relation in regard to `Req2`, then we can conclude that all operations are disabled in <math>s_7</math> except for `Rel1`. Thus, in this case we saved up one guard test more in comparison to the depth-first search example.

	[[ file: StateSpaceBreadthFirst.png ]]		[[ file: StateSpaceBreadthFirst.png ]]

Ivaylo Dobrikov: /* Partial Guard Evaluation */

2015-09-07T09:01:06Z

Partial Guard Evaluation

← Older revision		Revision as of 09:01, 7 September 2015
Line 120:		Line 120:
	where the green boxes denote that the evaluation of the guard of <tt>Op2</tt> is true, whereas the red boxes indicate that the evaluation of the guard of <tt>Op2</tt> is false.		where the green boxes denote that the evaluation of the guard of <tt>Op2</tt> is true, whereas the red boxes indicate that the evaluation of the guard of <tt>Op2</tt> is false.

	The model checker optimization, partial guard evaluation, makes use of such kind of relations. The enabling relations are determined by means of syntactic and constraint-based analyses. In particular, we concentrate on three kinds of enabling relations:		The model checker optimization, partial guard evaluation, makes use of such a kind of relations. The enabling relations are determined by means of syntactic and constraint-based analyses. In particular, we concentrate on three kinds of enabling relations:
	*[[file: GuaranteedRelation.png]] <br/><tt>Op2</tt> is '''always''' enabled after the execution of <tt>Op1</tt>		*[[file: GuaranteedRelation.png]] <br/><tt>Op2</tt> is '''always''' enabled after the execution of <tt>Op1</tt>
	*[[file: ImpossibleRelation.png]] <br/><tt>Op2</tt> is '''impossible''' to be enabled after the execution of <tt>Op1</tt>		*[[file: ImpossibleRelation.png]] <br/><tt>Op2</tt> is '''impossible''' to be enabled after the execution of <tt>Op1</tt>