In this post, we will talk about fairness both weak and strong. Every program has a skip action and every program has multiple actions. In an informal model, we reach into a hat and pick an action. If we are very unlucky we pick the skip action over and over again. None of the others are ever chosen and the program does nothing. To prevent this kind of selection, we impose a fairness requirement on the selection of actions. There are two kinds of fairness - weak and strong.
Under weak fairness, every action is guaranteed to be selected infinitely often. Said another way between any two selections of the same action, there are a finite number of selections of other actions. There is no however guarantee how many actions may be selected before all actions have been selected at least once.
In we take an example where the program maintains a state based on a boolean variable and increments a counter modulo four times. b is assigned the result of the modulo. If n is zero, the boolean is assigned false.
A directed graph can be drawn representing the program with the vertex as states of the program and the directed edges representing the actions. So weak fairness says that each edge label is guaranteed to repeat often in an infinite path.
If the program begins execution in a state satisfying the predicate n = 1, the initial state is <false,1> and then each possible computation leaves the state unchanged. If on the other hand, the initial state is the state <true, 1>, then there is no guarantee the state reaches the fix point of <false, 1> and it cycles repeatedly between <true,1>, <true, 2>, <true, 3> and <true, 0>. The action that assigns false to b must be selected an infinite number of times, but it may be selected every time n = 3 and the action has no effect. In such a program, every action is selected infinitely often and this satisfies the weak requirement.
Under strong fairness, in addition to the weakness requirement, if an action is enabled infinitely often, it is selected infinitely often. Note that in the previous example, the selection was extraordinarily unlucky because one action was only chosen at particular times when it happens to be unenabled. In the strong fairness program, the cycle would not be allowed to repeat without selecting the action that assigns false to b. This program could then be guaranteed to reach the fixed point and terminate.
In general, if we come up with a property for a program then that property holds regardless of whether the actual execution is weak or strong. However is a property relies on strong fairness, that property may or may not hold for weak fairness. The program could choose to assume weak fairness.
Under weak fairness, every action is guaranteed to be selected infinitely often. Said another way between any two selections of the same action, there are a finite number of selections of other actions. There is no however guarantee how many actions may be selected before all actions have been selected at least once.
In we take an example where the program maintains a state based on a boolean variable and increments a counter modulo four times. b is assigned the result of the modulo. If n is zero, the boolean is assigned false.
A directed graph can be drawn representing the program with the vertex as states of the program and the directed edges representing the actions. So weak fairness says that each edge label is guaranteed to repeat often in an infinite path.
If the program begins execution in a state satisfying the predicate n = 1, the initial state is <false,1> and then each possible computation leaves the state unchanged. If on the other hand, the initial state is the state <true, 1>, then there is no guarantee the state reaches the fix point of <false, 1> and it cycles repeatedly between <true,1>, <true, 2>, <true, 3> and <true, 0>. The action that assigns false to b must be selected an infinite number of times, but it may be selected every time n = 3 and the action has no effect. In such a program, every action is selected infinitely often and this satisfies the weak requirement.
Under strong fairness, in addition to the weakness requirement, if an action is enabled infinitely often, it is selected infinitely often. Note that in the previous example, the selection was extraordinarily unlucky because one action was only chosen at particular times when it happens to be unenabled. In the strong fairness program, the cycle would not be allowed to repeat without selecting the action that assigns false to b. This program could then be guaranteed to reach the fixed point and terminate.
In general, if we come up with a property for a program then that property holds regardless of whether the actual execution is weak or strong. However is a property relies on strong fairness, that property may or may not hold for weak fairness. The program could choose to assume weak fairness.
No comments:
Post a Comment