Derivation of A Simplified Reachable State Graph

IF (A repeated read pattern exists in ESi) THEN

Find the first repeated read pattern in ESi. Assume that it is R, and that R repeats n times.

Remove the first n–1 Rs from PG.

RETURN True.

ELSE

/* No more repeated read patterns in ESi */

RETURN False.

END }

5.6. Derivation of A Simplified Reachable State Graph

Although dynamic effective testing does not need a reachable state graph to explore the interleavings of the execution of the target concurrent program, the effective test sets obtained from dynamic effective testing can be used to derive the reachable state graph defined in Theorem 4, which we can then use to perform program debugging. Each SYN-sequence in an effective test set represents a part of a simplified reachable state graph. Generating SYN-sequences in dynamic effective testing represents generating this graph on the fly. The programmer can check the reachable state graph to determine if any erroneous state would be reached [68]. Also, the order of state transitions in the reachable state graph reveals possible interleavings of events. Once an unexpected state is found in the reachable state graph, the programmer can easily obtain the corresponding interleavings of processes that would make the execution reach the erroneous state, and then correct the program accordingly. Garg presented how to

80

enumerate consistent global states from a distributed computation [69]. The distributed computation contains sending and receiving events. The states in our simplified reachable state graph are defined in Definition 4 and are thus different from their

Figure 28. The simplified reachable state graph of the execution of the concurrent program shown in Figure 1A

Because we apply the ASET rules to transform the target concurrent program, only write operations to local and shared variables and read operations of shared variables are recorded in the SYN-sequence according to ASET rules 1 and 2. For example, for the concurrent program shown in Figure 1A, we only record operations in S0,0 and S1,0. Since not all the statements are recorded in the SYN-sequence, it is impossible to derive the complete reachable state graph if we apply the ASET rules. We overcome this limitation by deriving a simplified reachable state graph. Figure 28 shows the simplified reachable state graph of the concurrent program in Figure 1A. The complete reachable state graph of this program, which is shown in Figure 16, has eight states: Q0, Q1, …, Q7. Because S0,1 only contains local variable reads and the evaluation of Boolean predicates, its operation is not recorded in the SYN-sequence. Thus, we cannot derive states Q3, Q6, and Q7 from SYN-sequences in the effective test set. Actually, a simplified reachable state graph of a concurrent program P with X contains states after the execution of events including write operations to local and shared variables as well as read operations of

shared variables. Because only the read and write operations of a shared variable race, it is sufficient for the programmer to observe the interleaving of synchronization events in the simplified reachable state graph. These states that are absent from the simplified reachable state graph are called not-synchronization-related states. Fortunately, all the not-synchronization-related states can be derived from the simplified reachable state graph and the source code of the target concurrent program, since statements that are ignored by the ASET rules do not race with other statements. For example, consider state Q1 {(S0,0,START), (a=0, t=0)} in Figure 28. This simplified reachable state graph reveals that process P0 may perform statement S0,0 and then stay in Q1. However, according to the semantics of this program, the next statement executed by P0 after state Q1 is S0,1. Since the execution of S0,1 only changes the execution location of P0 from S0,0

to S0,1, we know that P0 first executes S0,1 and then transits to state {(S0,1,START), (a=0,t=0)}, which is state Q3 shown in Figure 16. P0 then executes statement S0,0 and returns to Q1. We obtain that the state transition from Q1 back to Q1 by statement S0,0 in the simplified reachable state graph actually skips a not-synchronization-related state Q3. Since all of the not-synchronization-related states can be derived, the simplified reachable state graph contains sufficient information for the programmer to observe the behavior of the program for code debugging.

Note that we still can achieve the state-cover goal in dynamic effective testing despite applying the ASET rules to simplify the SYN-sequence. Assume that a concurrent program is transformed based on ASET rules. The dynamic behavior between events stored in its SYN-sequence is deterministic since statements between these events do not race with other statements. Thus, we can consider that all the

82

not-synchronization-related states will be executed during dynamic effective testing, and it is obvious that we can derive them from the simplified reachable state graph.

Algorithm 9 can construct a DFA from the effective test sets produced by dynamic effective testing. As mentioned in Section 5.2, we can generate totally ordered sequences of events from SYN-sequences to obtain execution states. However, since a single totally ordered sequence of events derived from a SYN-sequence cannot display all the execution states, as shown in Figure 26, we instead explore all the valid totally ordered sequences of events for the SYN-sequences in the effective test set. We consider the execution states derived from a SYN-sequence S are covered during the dynamic testing which generates S. Note that we do not define if the DFA derived by Algorithm 9 is a complete or a simplified reachable state graph. If we apply the ASET rules to collect synchronization events, then the derived DFA is the simplified reachable state graph.

However, if we also record not-synchronization-related events in the SYN-sequence, we can obtain a complete reachable state graph.

Algorithm 9: Construct a DFA from an effective test set Input: An effective test set ET.

Output: A DFA F where each state in F is labeled with an execution-location vector and a variable-value vector, and transitions are labeled with events.

(1) Add an initial state X0 in which each element in the execution-location vector is marked “START”, which means that none of the statements are executed and each element in the variable-value vector stores the initial value of the corresponding variable.

(2) FOR each SYN-sequence S in ET

Generate all the valid totally ordered sequences of events of S. Define TOSS as the set containing all the totally ordered sequences of events of S.

FOR each totally ordered sequence of events Z in TOSS

Assume that there are n events in Z, which have the order e0, e1, …, en–1. FOR i=0 to n–1

• Let state Xi+1 be the execution state after the execution of event ei.

• Add Xi+1 as a state in F if Xi+1 is not in F.

• Add a transition from Xi to Xi+1 and label it with ei if this transition does not exist in F.

END FOR END FOR END FOR

For example, Figure 29 is the simplified reachable state graph derived by an effective test set of the concurrent program shown in Figure 23²¹. C1=“Q2, Q19”, C2=“Q5, Q6”, C3=“Q17, Q16”, C4=“Q14, Q18”, C5=“Q14, Q15, Q26, Q18”, and C6=“Q14, Q15, Q26, Q27” are several cycles in this DFA.

21 The graph was generated using our software tool (see Chapter 7).

Figure 29. The simplified reachable state graph of the execution of the concurrent

However, Algorithm 9 has E are the number of SYN events in the SYN-sequences

occur if the DFA has a huge number of states.

84

The simplified reachable state graph of the execution of the concurrent program shown in Figure 23

has exponential complexity defined as O(N×P are the number of SYN-sequences, number of processes, and maxim

sequences, respectively. It is obvious that a state-space explosion a huge number of states.

The simplified reachable state graph of the execution of the concurrent

P^E), where N, P, and sequences, number of processes, and maximum number of space explosion can

85