Mutual Exclusion (Fairness) - Revision history

Ivaylo Dobrikov at 08:58, 13 January 2015

2015-01-13T08:58:43Z

← Older revision		Revision as of 08:58, 13 January 2015
Line 15:		Line 15:

	(FG e(Req1) => GF [Req1]) & (GF e(Enter1) => GF [Enter1]) => GF {p1 = crit1}		(FG e(Req1) => GF [Req1]) & (GF e(Enter1) => GF [Enter1]) => GF {p1 = crit1}
	For checking the formula the LTL model checker generates 13312 atoms<ref>The number of atoms generated for the search graph corresponds to the number of valuations of the respective LTL<sup>e</sup> formula times the number of states of the model.</ref> and 7515 transitions and needs overall 509 ms to prove the property (the model has 8 states and 15 transitions in total). On the other hand, using the extension of the LTL model checker for checking fairness (by entering the formula `WF(Req1) & SF(Enter1) => GF {p1=crit1}`), the model checker generates 32 atoms and 39 transitions (the atoms and transitions generated just for `GF {p1 = crit1}`) and an overall time of 50 ms.		For checking the formula the LTL model checker generates 13312 atoms<ref>The number of atoms generated for the search graph corresponds to the number of valuations of the respective LTL<sup>[e]</sup> formula times the number of states of the model.</ref> and 7515 transitions and needs overall 509 ms to prove the property (the model has 8 states and 15 transitions in total). On the other hand, using the extension of the LTL model checker for checking fairness (by entering the formula `WF(Req1) & SF(Enter1) => GF {p1=crit1}`), the model checker generates 32 atoms and 39 transitions (the atoms and transitions generated just for `GF {p1 = crit1}`) and an overall time of 50 ms.

	For checking the requirement ''each process will enter infinitely often its critical section'' the LTL formula ` GF {p1 = crit1} & GF {p2 = crit2}` should be checked with the following fairness constraints:		For checking the requirement ''each process will enter infinitely often its critical section'' the LTL formula ` GF {p1 = crit1} & GF {p2 = crit2}` should be checked with the following fairness constraints:

Ivaylo Dobrikov at 16:49, 12 January 2015

2015-01-12T16:49:19Z

← Older revision		Revision as of 16:49, 12 January 2015
Line 15:		Line 15:

	(FG e(Req1) => GF [Req1]) & (GF e(Enter1) => GF [Enter1]) => GF {p1 = crit1}		(FG e(Req1) => GF [Req1]) & (GF e(Enter1) => GF [Enter1]) => GF {p1 = crit1}
	For checking the formula the LTL model checker generates 13312 atoms<ref>The number of atoms generated for the search graph corresponds to the number of valuations of the respective LTL formula times the number of states of the model.~~<sup>e</sup>~~</ref> and 7515 transitions and needs overall 509 ms to prove the property (the model has 8 states and 15 transitions in total). On the other hand, using the extension of the LTL model checker for checking fairness (by entering the formula `WF(Req1) & SF(Enter1) => GF {p1=crit1}`), the model checker generates 32 atoms and 39 transitions (the atoms and transitions generated just for `GF {p1 = crit1}`) and an overall time of 50 ms.		For checking the formula the LTL model checker generates 13312 atoms<ref>The number of atoms generated for the search graph corresponds to the number of valuations of the respective LTL<sup>e</sup> formula times the number of states of the model.</ref> and 7515 transitions and needs overall 509 ms to prove the property (the model has 8 states and 15 transitions in total). On the other hand, using the extension of the LTL model checker for checking fairness (by entering the formula `WF(Req1) & SF(Enter1) => GF {p1=crit1}`), the model checker generates 32 atoms and 39 transitions (the atoms and transitions generated just for `GF {p1 = crit1}`) and an overall time of 50 ms.

	For checking the requirement ''each process will enter infinitely often its critical section'' the LTL formula ` GF {p1 = crit1} & GF {p2 = crit2}` should be checked with the following fairness constraints:		For checking the requirement ''each process will enter infinitely often its critical section'' the LTL formula ` GF {p1 = crit1} & GF {p2 = crit2}` should be checked with the following fairness constraints:

Ivaylo Dobrikov at 16:47, 12 January 2015

2015-01-12T16:47:43Z

← Older revision		Revision as of 16:47, 12 January 2015
Line 15:		Line 15:

	(FG e(Req1) => GF [Req1]) & (GF e(Enter1) => GF [Enter1]) => GF {p1 = crit1}		(FG e(Req1) => GF [Req1]) & (GF e(Enter1) => GF [Enter1]) => GF {p1 = crit1}
	For checking the formula the LTL model checker generates 13312 atoms and 7515 transitions and needs overall 509 ms to prove the property (the model has 8 states and 15 transitions in total). On the other hand, using the extension of the LTL model checker for checking fairness (by entering the formula `WF(Req1) & SF(Enter1) => GF {p1=crit1}`), the model checker generates 32 atoms and 39 transitions (the atoms and transitions generated just for `GF {p1 = crit1}`) and an overall time of 50 ms.		For checking the formula the LTL model checker generates 13312 atoms<ref>The number of atoms generated for the search graph corresponds to the number of valuations of the respective LTL formula times the number of states of the model.<sup>e</sup></ref> and 7515 transitions and needs overall 509 ms to prove the property (the model has 8 states and 15 transitions in total). On the other hand, using the extension of the LTL model checker for checking fairness (by entering the formula `WF(Req1) & SF(Enter1) => GF {p1=crit1}`), the model checker generates 32 atoms and 39 transitions (the atoms and transitions generated just for `GF {p1 = crit1}`) and an overall time of 50 ms.

	For checking the requirement ''each process will enter infinitely often its critical section'' the LTL formula ` GF {p1 = crit1} & GF {p2 = crit2}` should be checked with the following fairness constraints:		For checking the requirement ''each process will enter infinitely often its critical section'' the LTL formula ` GF {p1 = crit1} & GF {p2 = crit2}` should be checked with the following fairness constraints:

Ivaylo Dobrikov at 16:32, 12 January 2015

2015-01-12T16:32:23Z

← Older revision		Revision as of 16:32, 12 January 2015
Line 15:		Line 15:

	(FG e(Req1) => GF [Req1]) & (GF e(Enter1) => GF [Enter1]) => GF {p1 = crit1}		(FG e(Req1) => GF [Req1]) & (GF e(Enter1) => GF [Enter1]) => GF {p1 = crit1}
	For checking the formula the LTL model checker generates 13312 atoms and 7515 transitions and needs overall 509 ms to prove the property. On the other hand, using the extension of the LTL model checker for checking fairness (by entering the formula `WF(Req1) & SF(Enter1) => GF {p1=crit1}`), the model checker generates 32 atoms and 39 transitions (the atoms and transitions generated just for `GF {p1 = crit1}`) and an overall time of 50 ms.		For checking the formula the LTL model checker generates 13312 atoms and 7515 transitions and needs overall 509 ms to prove the property (the model has 8 states and 15 transitions in total). On the other hand, using the extension of the LTL model checker for checking fairness (by entering the formula `WF(Req1) & SF(Enter1) => GF {p1=crit1}`), the model checker generates 32 atoms and 39 transitions (the atoms and transitions generated just for `GF {p1 = crit1}`) and an overall time of 50 ms.

	For checking the requirement ''each process will enter infinitely often its critical section'' the LTL formula ` GF {p1 = crit1} & GF {p2 = crit2}` should be checked with the following fairness constraints:		For checking the requirement ''each process will enter infinitely often its critical section'' the LTL formula ` GF {p1 = crit1} & GF {p2 = crit2}` should be checked with the following fairness constraints:

Ivaylo Dobrikov at 16:22, 12 January 2015

2015-01-12T16:22:56Z

← Older revision		Revision as of 16:22, 12 January 2015
Line 20:		Line 20:

	(WF(Req1) & WF(Req2)) & (SF(Enter1) & SF(Enter2))		(WF(Req1) & WF(Req2)) & (SF(Enter1) & SF(Enter2))
	Encoding these fairness conditions as an LTL<sup>[e]</sup> formula will blow up exponentially the number of atoms and the transitions and thus make practically impossible to check the above property in a reasonable time.		Encoding these fairness conditions as an LTL<sup>[e]</sup> formula will blow up exponentially the number of atoms and the transitions in regard to the number of temporal operators (in this case `G` (globally) and `F`(finally)) and thus make practically impossible to check the above property in a reasonable time.

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

Ivaylo Dobrikov at 16:17, 12 January 2015

2015-01-12T16:17:29Z

← Older revision		Revision as of 16:17, 12 January 2015
Line 12:		Line 12:
	Running the LTL model checker of ProB will provide for the last two properties above a counterexample since the model permits that a process may perform infinitely often consecutively the events ''request'', ''enter'' and ''release'', and in this way to ignore the other process infinitely. An example trace that describes this behavior could be <math>\langle Req2,Req1,Enter1,Rel1,Req1,Enter1,\ldots\rangle</math>.		Running the LTL model checker of ProB will provide for the last two properties above a counterexample since the model permits that a process may perform infinitely often consecutively the events ''request'', ''enter'' and ''release'', and in this way to ignore the other process infinitely. An example trace that describes this behavior could be <math>\langle Req2,Req1,Enter1,Rel1,Req1,Enter1,\ldots\rangle</math>.

	On the other hand, such behaviors can be considered as unrealistic computations for the eventual implementation of the algorithm. Therefore fairness constraints can be set in order to discard such behaviors. For example, checking the property ''process <math>P_1</math> will enter its critical section infinitely often'' (as LTL property: `GF {p1 = crit1}`) can be checked by restricting that the event `Req1` will not be continuously ignored and that the event `Enter1` will not be ignored infinitely often. Both conditions for the property can be given by means of an LTL<sup>[e]</sup> formula on the left side of the implication:		On the other hand, such behaviors can be considered as unrealistic computations for the eventual implementation of the algorithm. Therefore fairness constraints can be set in order to discard such behaviors. For example, checking the property ''process <math>P_1</math> will enter its critical section infinitely often'' (as LTL property: `GF {p1 = crit1}`) can be checked by restricting that the event `Req1` will not be continuously ignored and that the event `Enter1` will not be ignored infinitely often. Both conditions for the property can be given by means of an LTL<sup>[e]</sup> formula on the left side of the following implication:

	(FG e(Req1) => GF [Req1]) & (GF e(Enter1) => GF [Enter1]) => GF {p1 = crit1}		(FG e(Req1) => GF [Req1]) & (GF e(Enter1) => GF [Enter1]) => GF {p1 = crit1}

Ivaylo Dobrikov at 16:16, 12 January 2015

2015-01-12T16:16:33Z

← Older revision		Revision as of 16:16, 12 January 2015
Line 12:		Line 12:
	Running the LTL model checker of ProB will provide for the last two properties above a counterexample since the model permits that a process may perform infinitely often consecutively the events ''request'', ''enter'' and ''release'', and in this way to ignore the other process infinitely. An example trace that describes this behavior could be <math>\langle Req2,Req1,Enter1,Rel1,Req1,Enter1,\ldots\rangle</math>.		Running the LTL model checker of ProB will provide for the last two properties above a counterexample since the model permits that a process may perform infinitely often consecutively the events ''request'', ''enter'' and ''release'', and in this way to ignore the other process infinitely. An example trace that describes this behavior could be <math>\langle Req2,Req1,Enter1,Rel1,Req1,Enter1,\ldots\rangle</math>.

	On the other hand, such behaviors can be considered as unrealistic computations for the eventual implementation of the algorithm. Therefore fairness constraints can be set in order to discard such behaviors. For example, checking the property ''process <math>P_1</math> will enter its critical section infinitely often'' (as LTL property: `GF {p1 = crit1}`) can be checked by restricting that the event `Req1` will not be continuously ignored and that the event `Enter1` will not be ignored infinitely often. Both conditions on the property can be given by means of an LTL<sup>[e]</sup> formula on the ~~right~~ side of the implication ~~as follows~~:		On the other hand, such behaviors can be considered as unrealistic computations for the eventual implementation of the algorithm. Therefore fairness constraints can be set in order to discard such behaviors. For example, checking the property ''process <math>P_1</math> will enter its critical section infinitely often'' (as LTL property: `GF {p1 = crit1}`) can be checked by restricting that the event `Req1` will not be continuously ignored and that the event `Enter1` will not be ignored infinitely often. Both conditions for the property can be given by means of an LTL<sup>[e]</sup> formula on the left side of the implication:

	(FG e(Req1) => GF [Req1]) & (GF e(Enter1) => GF [Enter1]) => GF {p1 = crit1}		(FG e(Req1) => GF [Req1]) & (GF e(Enter1) => GF [Enter1]) => GF {p1 = crit1}

Ivaylo Dobrikov: Created page with 'Consider an Event-B model formalizing an algorithm for mutual exclusion with semaphores for two concurrent processes $P_1$ and $P_2$ . Each process has been …'

2015-01-12T15:44:59Z

Created page with 'Consider an Event-B model formalizing an algorithm for mutual exclusion with semaphores for two concurrent processes <math>P_1</math> and <math>P_2</math>. Each process has been …'

New page

Consider an Event-B model formalizing 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 events: ''request'' (for entering in the critical section), ''enter'' (entering the critical section), and ''release'' (exiting the critical section). (For more information on the algorithm and the design of the model see <ref>C.Baier and J.-P. Katoen. “Principles of Model Checking”, The MIT Press, 2008, pages 43-45.</ref>).

Each of the actions of a process are represented by a respective event:

 [[File:LTLViewMUTEXEvents.png|center|600px]] 

Each process <math>P_i</math> has three possible states that are denoted by the constants <math>noncrit_{i}</math> (the state in which <math>P_i</math> performs noncritical actions), <math>wait_{i}</math> (the state in which <math>P_{i}</math> waits to enter the critical section), and <math>crit_{i}</math> (representing the state in which <math>P_{i}</math> is in the critical section). Both processes share the binary semaphore y where y=1 indicates that the semaphore is free and y=0 that the semaphore is currently processed by one of the processes.

There are several requirements that the mutual exclusion algorithm should satisfy. The most important one is the mutual exclusion property that says ''always at most one process is in its critical section''. This can be simply expressed, for example, as an invariant of the respective Event-B model: not(p1 = crit1 & p2 = crit2). However, there are other properties that can be easily expressed by means of LTL formulas and automatically checked on the model. For example, the requirement ''each process will enter infinitely often its critical section'' can be specified by the LTL formula `GF {p1 = crit1} & GF {p2 = crit2}` or the starvation freedom property that states ''each waiting process will eventually enter its critical section'':

G ({p1 = wait1} => F {p1 = crit1}) & G ({p2 = wait2} => F {p2=crit2})
Running the LTL model checker of ProB will provide for the last two properties above a counterexample since the model permits that a process may perform infinitely often consecutively the events ''request'', ''enter'' and ''release'', and in this way to ignore the other process infinitely. An example trace that describes this behavior could be <math>\langle Req2,Req1,Enter1,Rel1,Req1,Enter1,\ldots\rangle</math>.

On the other hand, such behaviors can be considered as unrealistic computations for the eventual implementation of the algorithm. Therefore fairness constraints can be set in order to discard such behaviors. For example, checking the property ''process <math>P_1</math> will enter its critical section infinitely often'' (as LTL property: `GF {p1 = crit1}`) can be checked by restricting that the event `Req1` will not be continuously ignored and that the event `Enter1` will not be ignored infinitely often. Both conditions on the property can be given by means of an LTL[e] formula on the right side of the implication as follows:

(FG e(Req1) => GF [Req1]) & (GF e(Enter1) => GF [Enter1]) => GF {p1 = crit1}
For checking the formula the LTL model checker generates 13312 atoms and 7515 transitions and needs overall 509 ms to prove the property. On the other hand, using the extension of the LTL model checker for checking fairness (by entering the formula `WF(Req1) & SF(Enter1) => GF {p1=crit1}`), the model checker generates 32 atoms and 39 transitions (the atoms and transitions generated just for `GF {p1 = crit1}`) and an overall time of 50 ms.

For checking the requirement ''each process will enter infinitely often its critical section'' the LTL formula ` GF {p1 = crit1} & GF {p2 = crit2}` should be checked with the following fairness constraints:

(WF(Req1) & WF(Req2)) & (SF(Enter1) & SF(Enter2))
Encoding these fairness conditions as an LTL[e] formula will blow up exponentially the number of atoms and the transitions and thus make practically impossible to check the above property in a reasonable time.

== References ==
<references/>