7.3 Liveness

7.3 Liveness

A liveness property asserts that something good eventually happens. A reasonable liveness property for the single-lane bridge would be that all red and blue cars eventually get to cross the bridge. As we have seen, the program developed in the previous section does not satisfy this property in the situation where there are three cars of each type. In this section, we see how models can be analyzed for liveness. Like deadlock and other safety properties, the objective is to solve liveness problems at the modeling stage so that they do not occur in the implemented program.

A completely general treatment of liveness is rather involved and requires the use of a temporal logic to specify the required liveness properties. Rather than burden the reader with another formalism, we deal with a restricted class of liveness properties which we term progress. A progress property asserts that whatever state a system is in, it is always the case that a specified action will eventually be executed. Progress is the opposite of starvation, the name given to a concurrent-programming situation in which an action is never executed. Progress properties are simple to specify and are sufficiently powerful to capture a wide range of liveness problems in concurrent programs.

7.3.1 Progress Properties

To illustrate the notion of progress, we use a simple example, that of tossing a coin. The model is depicted in Figure 7.8.

Figure 7.8: COIN model.

If the coin were tossed an infinite number of times, we would expect that heads would be chosen infinitely often and that tails would be chosen infinitely often. In fact, this depends on the scheduling policy used to decide on which transition from the set of eligible transitions should be executed. If the policy is not fair then we could always choose the toss transition leading to heads. We assume that the scheduling policy for choice is fair as defined in the following:

Fair Choice: If a choice over a set of transitions is executed infinitely often, then every transition in the set will be executed infinitely often.

If the transition (or transitions) of an action occurs infinitely often in a system, we can say that it is always the case at any stage of the execution that the action will eventually occur. With the assumption of fair choice then the coin-tossing system should eventually choose heads and eventually choose tails. We can assert this with progress properties specified in FSP. A progress property is defined by:

progress P = {a₁,a₂..a_n} defines a progress property P which asserts that in an infinite execution of a target system, at least one of the actions a₁,a₂..a_n will be executed infinitely often.

In other words, a progress property asserts that at any stage of execution one of the actions in the progress set will eventually occur. The liveness requirement for coin tossing can now be expressed as:

 progress HEADS = {heads} progress TAILS = {tails}

The COIN system we have defined so far satisfies these properties. We now examine a system that does not. Suppose that the agent which tosses the coin first picks one of two coins: a normal coin with a head and a tail as defined in Figure 7.8 and a trick coin which has a head on both sides. The outcome of tossing the trick coin must always be heads. This system is modeled in Figure 7.9.

Figure 7.9: TWOCOIN model.

Progress analysis of the TWOCOIN system against the progress properties HEADS and TAILS produces the following output:

 Progress violation: TAILS Path to terminal set of states:      pick Actions in terminal set: {toss, heads}

This confirms the expected result: if the agent picks the trick coin then the action tails will never occur. This is of course a violation of the TAILS progress property, which asserts that in an infinite execution, tails must occur infinitely often. The reader should note that the system of Figure 7.9 does not violate the progress property:

 progress HEADSorTAILS = {heads,tails}

Property HEADSorTAILS is not violated since only one of the actions in the progress set need be executed infinitely often to satisfy the property.

7.3.2 Progress Analysis

Progress analysis involves first performing a search for terminal sets of states.

A terminal set of states is one in which every state is reachable from every other state in the set via one or more transitions and there is no transition from within the set to any state outside the set.

In graph theory, this is known as a strongly connected component, which has no path to any nodes outside the set of nodes in the component. For example, the labeled transition system of Figure 7.9 has two terminal sets of states,{1, 2}, which are the states relating to the trick coin, and {3, 4, 5}, which are the states relating to the normal coin.

An execution of a system represented by a finite set of states can only be infinite if some of the states are visited infinitely often. The states that are visited infinitely often in an execution must form a terminal set. Given fair choice, each terminal set of states represents an execution in which each transition in the set is executed infinitely often. Since there is no transition out of a terminal set, any action that is not used in all terminal sets cannot occur infinitely often in all executions of the system. Checking that a progress property holds is now simply checking that in each terminal set, at least one of the actions in the progress set occurs as a transition. Conversely, a progress property is violated if analysis finds a terminal set of states in which none of the progress set actions appear. For the TAILS property, this terminal set is the set of states {1, 2} in which the action tails does not occur. The output gives the shortest execution path to the root of the terminal set and lists the actions that do appear in the set.

If no progress properties are specified, LTSA performs progress analysis using a default property. This property asserts that for every action in the alphabet of the target system, given fair choice, that action will be executed infinitely often. This is equivalent to specifying a separate progress property for every action. For the TWOCOIN system, this default analysis produces the following output:

 Progress violation for actions: {pick} Path to terminal set of states:      pick Actions in terminal set: {toss, heads, tails} Progress violation for actions: {pick, tails} Path to terminal set of states:      pick Actions in terminal set: {toss, heads}

The analysis produces two progress violations since the action pick is not executed infinitely often in either terminal set. The value of this default property is that if it is not violated, then no specified progress properties can be violated. In other words, if the default property holds, then every other progress property, specified in terms of subsets of the action alphabet of a target system, must also hold. This is true since the default property asserts that every action is executed infinitely often. All systems in which the states occur inside a single terminal set satisfy the default progress property.

7.3.3 Action Priority

If default progress analysis is applied to the single-lane bridge model then no violations are detected. However, we know from the implementation that it is possible for progress violations to occur. Either the blue cars or the red cars may wait forever to cross the bridge. Why do we not detect these progress problems?

The answer lies in the fair choice assumption underlying the progress test. This means that every possible execution of the system will eventually happen including those in which cars do not starve. To detect progress problems we must superimpose some scheduling policy for actions, which models the situation in which the bridge is heavily used, i.e. we need to impose adverse conditions which “stress-test” the system. We use action priority expressions to describe these scheduling policies. Action priority is specified in FSP with respect to process compositions.

High Priority Operator (“<<”)

||C = (P||Q) <<{a₁,...,a_n} specifies a composition in which the actions a₁,...,a_n have higher priority than any other action in the alphabet of P||Q including the silent action tau. In any choice in this system which has one or more of the actions a₁,...,a_n labeling a transition, the transitions labeled with lower priority actions are discarded.

Low Priority Operator (“>>”)

||C = (P||Q)>>{a₁ ,...,a_n } specifies a composition in which the actions a₁,...,a_n have lower priority than any other action in the alphabet of P||Q including the silent action tau. In any choice in this system which has one or more transitions not labeled by a₁,...,a_n, the transitions labeled by a₁,...,a_n are discarded.

Action priority operators simplify the composite processes by discarding particular transitions. Figure 7.10 illustrates the effect for a simple example. When work is specified to be a high priority action in the composition HIGH, the sleep transition disappears since it is lower priority and consequently in a choice between sleep and work, work will always be chosen. When work is specified to be a low priority action in the composition LOW, the work transition disappears since it is lower priority and consequently in a choice between sleep and work, sleep will always be chosen.

Figure 7.10: Action priority.