The framework for dynamic effective testing

We developed a scheme for implementing dynamic effective testing. Since our goal was to perform source-code-level dynamic testing on concurrent programs, static analysis of the source codes was not allowed. Figure 17 shows the proposed framework for conducting dynamic effective testing. First, the SYN-sequences generated during testing are analyzed and transformed before they are processed by the race analyzer; this avoids boundless state reiteration. We have to obtain a sequence of execution states from a SYN-sequence so that we can identify reiterated states from them. According to these identified reiterated states, we may either truncate some events from the SYN-sequence or abandon the entire SYN-sequence. Note that the truncation of events and abandonment of SYN-sequences cannot be too aggressive so as to cause some states or transitions not to be traversed during the testing process. Second, the transformed SYN-sequence is analyzed to derive race variants by the race analyzer, with the aim of exploring different interleavings of the concurrent program in dynamic testing. Finally, we perform prefix-based replay of the race variants that are prefixes of some feasible SYN-sequences.

The derivation of race variants to explore different interleavings of concurrent program during dynamic effective testing originates from reachability testing, and prefix-based replay is a well-known method used in the deterministic testing of concurrent programs.

However, we have to confirm that the previous developed scheme used by the race analyzer is sufficient to achieve the goal of state-cover testing. In addition, the traditional prefix-based replay does not record sufficient information about synchronization events to support the SYN-sequence transformation. We also studied

how to improve this situation.

Execution of P with input X

Race analyzer (To derive race variants)

Queue to store race variants

Prefix-based replay of R

...

A SYN-sequence S

Derived race variants

Removed a race variant R from the queue Obtained a SYN-sequence

SYN-sequence transformation function

Transformed SYN-sequence Check if it is a new

SYN-sequence

Yes

No Discard the SYN-sequence

Figure 17. The proposed framework for dynamic effective testing 5.3. Transformation of SYN-sequences to implement dynamic effective testing

We develop a systematic scheme to avoid boundless state reiteration during testing.

Before each SYN-sequence is sent to the race analyzer, it is processed using a SYN-sequence transformation function Γ. The input argument of Γ is a SYN-sequence.

Before giving the formal proof to show that the Γ function can be used to implement dynamic effective testing, we first describe it abstractly.

Because we need to generate race variants to explore interleavings and execution states of the target concurrent program, we first describe how race variants are generated. At the beginning of the testing, the analysis delimiter @ is placed at the beginning of the SYN-sequence because all the events are collected during the monitor phase¹². Referring to Figure 18A, assume that X0, X1, …, Xi, …, XN–1 forms a totally ordered sequence of execution states¹³ of a SYN-sequence S, and Xk transits to Xk+1 by the

12 Events after the analysis delimiter @ are obtained in the monitor phase.

13 Although we can always derive multiple totally-ordered sequences of execution states from a SYN-sequence,

48

execution of a synchronization event ek, where 0≤k<N–2. X0 is the initial state and XN–1

is one of the final states. It is obvious that executions that exercise different SYN-sequences may bring the program execution to different final states. The race analyzer generates race variants by changing the synchronization event that is exercised from an execution state s, so that a new transition from state s is covered. We call it exploring interleavings in a state. For example, in execution state Xk, if there exists an event ex that can occur before ek but after Xk, then combining a list of events that occurred before Xk and event ex forms a race variant since the execution of this race variant will reach another execution state rather than state Xk+1. Note that if more than one event can occur before ek, then multiple race variants can be derived in state Xk. We denote the set of race variants that can be derived in state Xk as RV_Set(Xk). All the race variants that can then be derived from SYN-sequence S are RV_Set(X0) ∪ RV_Set(X1)

∪ … ∪ RV_Set(XN–2). Figure 18B shows a race variant V′ obtained in state Xi (V′∈

RV_Set(Xi)) and Figure 18C shows SYN-sequence S′ obtained from the prefix-based replay of V′. Note that X′≠Xi+1. For convenience, we call S the parent SYN-sequence of S′, S′ the child SYN-sequence of S, and V′ the originating race variant of S′.

Considering S′, since its parent SYN-sequence is S, we will also perform the prefix-based replay of RV_Set(X0) ∪ RV_Set(X1) ∪ … ∪ RV_Set(Xi). That is, the interleavings on execution states X0, X1, …, Xi will be explored in the race analysis of its parent SYN-sequence S. Thus, for a SYN-sequence T that is obtained from the prefix-based replay of a race variant, all possible interleavings of the states before @ (except the last state before @) will be explored in the race analysis of the ancestor

in Section 5.4.2 we prove that a single sequence is sufficient for the Γ function to avoid boundless state reiteration.

SYN-sequences of T. Refer to Figure 18A and Figure 18C. The possible interleavings of X0, X1, …, Xi in S′ were explored in the race analysis of S. Therefore, in the race analysis of S′ we only have to change the order of synchronization events which are after @ in S′. Note that state X′ is a new state in V′. We will explore the possible interleavings of V′ in the race analysis of S′ by changing the first synchronization event after @.

We assign a unique ID to each synchronization event when it is obtained in the monitor phase of the prefix-based replay. As we have mentioned, the execution of event ek–1

causes the execution state to transition to Xk. We define the associated event ID of state Xk to be the unique ID of ek–1. Most of the associated event IDs of execution states before @ are inherited from the corresponding states of the parent SYN-sequence. For example, the associated event IDs of X0, X1, …, and Xi in S and S′ are identical.

However, since state X′ in S′ is a new state after Xi, we must assign a unique associated event ID to X′ in S′. The associated event ID of a state in a SYN-sequence T is used to determine whether the state is inherited from the parent SYN-sequence of T. We use this information to determine whether a state is reiterated during testing.

50

Figure 18. Conventional operation of reachability testing to explore different interleavings and some examples

The basic idea is that we have to examine the execution states. When a state is found to appear multiple times in a SYN-sequence, the state is recorded. The stored reiterated states then are used to avoid boundless state reiteration. We employ two examples to demonstrate the basic idea. In the first example, we consider the program shown in Figure 1A. See the reachable state graph of it in Figure 16. S1={S0,0, S0,1,S1,0, S0,0, S0,1} shown in Figure 18D is a feasible totally order sequence of the execution of this program.

RV1={S0,0, S0,1, S0,0} in Figure 18E is one of the race variants derived in state Q3 and S1′

in Figure 18F is the SYN-sequence obtained by the prefix-based replay of RV1. S1 is the

parent SYN-sequence of S1′. Q1 is a reiterated state in S1′. Since all the possible interleavings after the first Q1 will be explored in the analysis of S1 and Q1 appears twice before @ in S1′, the analysis of events after the second Q1 in S1′ is redundant. We do not have to analyze events after @ in S1′. Thus, we should abandon the S1′. Actually, if we continue to explore interleavings after Q1 in S1′, it will cause boundless state reiteration.

In the second example, we use a program with a more complicated reachable state graph¹⁴. S2 shown in Figure 18G is a feasible totally order sequence of the execution of this program. RV2 in Figure 18H is one of the race variants derived in state Q0 and S2′ in Figure 18I is the SYN-sequence obtained by the prefix-based replay of RV2. S2 is a parent SYN-sequence of S2′. We can see that Q14 appears twice in S2. Of course, the possible interleavings after Q14 will be explored in the analysis of S2. Since we know that S2 is a parent SYN-sequence of S2′, we do not have to explore interleavings after Q14 in S2′. In fact, if we continue to explore interleavings after Q14 in S2′, it will cause boundless state reiteration. Thus, we should truncate the events after Q14, creating SYN-sequence S2′′, and generate race variants from S2′′ instead of S2′. We can also use S2 and S2′′ to illustrate the definition of associated event ID. The associated event ID of Q14 in S2′ is different from the associated event ID of the first Q14 in S2 as Q14 is reached by the execution of new events after @ in S2′. We can illustrate the Γ function, as done below.

Definition 6 defines the Γ function, which examines the execution states to avoid boundless state reiteration. This is accomplished by attaching a reiterated state set to

14 See the reachable state graph in Figure 29.

52

each SYN-sequence and race variant. When a state is found to appear multiple times in a SYN-sequence, it is added to this set. The reiterated state set attached to the SYN-sequence obtained from the prefix-based replay was inherited from its originating race variant. The race variants also inherit the reiterated state set from the SYN-sequence from which it was derived. In the definition of Γ, we use “A” and “αi” to denote the newly discovered reiterated state and previously found reiterated state, respectively.

Figure 19. Definition of the SYN-sequence transformation function Γ

There are several different cases for transforming a given SYN-sequence S. In cases 1 and 2 we discover one unrecorded reiterated state and add it to the reiterated state set of S. Referring to Figure 19, state A in cases 1 and 2 reiterates in SYN-sequence S. Note

that this may reveal multiple reiterated states in S. However, A is the first one to appear in S. We add state A to the reiterated state set and label it with the associated event ID of the first A. The subsequent race analysis of S1 or S2 will explore all the interleavings for state A. Since we can only discover one reiterated state in each invocation of the Γ function, other reiterated states will be added to the reiterated state set when we apply Γ′

or Γ′′ function to the descendant SYN-sequences of S in case 4 or 5B, respectively (for details, see Definition 6). In case 3, state A reiterated multiple times before @. Since the interleavings after state A will be explored in the race analysis of the parent SYN-sequence of S, we do not have to explore the interleavings after state A again in S.

Thus, S is abandoned in this case. This is the case where S1′ has to be abandoned as shown in Figure 18F.

In cases 4, 5A, 5B, and 6, state αi is a reiterated state found previously. In case 4, the first state αi occurs after @. State αi must then be a reiterated state where the first occurrence is after @ in the parent SYN-sequence of S as shown in SYN-sequence S1 of case 1.

Note that if αi was added to the reiterated state set in case 2, then the first occurrence of α_i must be before @. Since interleavings after reiterated state αi will be explored by the race analysis of its parent SYN-sequence, we do not need to analyze states after the newly discovered αi in this SYN-sequence. Instead we simply truncate all events that occurred after αi in case 4. The Γ′ function defined in case 4 will try to discover if there exists a new reiterated state in S4. This is the case where we remove events after Q14 in S2′ as shown in Figure 18I.

In cases 5A, 5B, and 6, state αi occurs before @. In cases 5A and 5B the previously

54

found reiterated state αi only appears once before @. We can use the associate event ID of αi to differentiate if αi is newly generated or from its parent SYN-sequence. In case 5A the associated event ID of αi in S differs from the labeled event ID of αi in the reiterated state set. The originating race variant R of S must be derived from case 1 by analyzing a state in Pe and the prefix-based replay of R produces state αi again. Since interleavings after reiterated state αi will be explored by the race analysis of its parent SYN-sequence, we abandon S. On the other hand, in case 5B the associated event ID of αi in S is identical to the labeled event ID of αi in the reiterated state set. The originating race variant of S is derived from case 1 by analyzing a state after the first A¹⁵ or from case 2 by analyzing a state in Pe. We have to continue exploring interleavings after the first A until we reach another A. The Γ′′ function defined in case 5B will try to discover if there exists a new reiterated state in S.

In case 6 there exist multiple previously found reiterated states αi before @, since the interleavings after state αi will be explored in the race analysis of its parent SYN-sequence of S. We do not have to continue to explore interleavings after αi again in this SYN-sequence. We therefore abandon S in case 6.

Definition 6: Let S be a SYN-sequence, and Γ: S→Z. Z is a set of SYN-sequences or the empty set. Note that S is attached to a reiterated state set, and elements in the reiterated state set are labeled with event IDs. It is easy to assign a unique ID to each event in S. S contains an analysis delimiter @. The synchronization events after @ are

15 Note that we add state A to the reiterated state set and label it with the associated event ID of the first A in cases 1 and 2.

obtained in the monitor phase of the prefix-based replay. Assume that the reiterated state set attached to S contains n states α0, α1, …, αn–1. Γ is defined as follows:

• Case 1: Referring to Figure 19A, α0, α1, …, αn–1 do not occur during the execution of S, and the execution after @ encounters some identical execution states multiple times, which are called reiterated states. It is possible that there are multiple reiterated states. We assume that A is the first one. We have Γ(S)={S1}, where S1 contains all the events in S. State A is added to the reiterated state set of S1, and A is labeled with the associated event ID of the first A.

• Case 2: Referring to Figure 19B, α0, α1,…, αn–1 do not occur during the execution of S, and the execution encounters some identical execution states multiple times. We assume that A is the first reiterated state. State A occurs before @ only once. We have Γ(S)={S2}, where state A is added to the reiterated state set of S2, and A is labeled with the associated event ID of the first A.

• Case 3: Referring to Figure 19C, α0, α1, …, αn–1 do not occur during the execution of S, and the execution encounters some identical execution states multiple times before @. We assume that A is the first reiterated state, and we have Γ(S)=∅.

• Case 4: Referring to Figure 19D, α0, α1, …, αn–1 do not occur before @, and ∃ αi, 0≤i<n, αi appears after @. Without loss of generality, we assume that αi is the first one. We have Γ(S)= Γ′(S4). S4 is obtained by removing all the events that occurred after αi. The Γ′ function is as follows:

 If there is no new reiterated state in S4, then we have Γ′(S4)=S4.

 If there is at least one new reiterated state in S4, then Γ′(S4) performs the same transformation as for cases 1, 2, and 3.

• Case 5A and 5B: Referring to Figure 19E, ∃ αi, 0≤i<n, αi appears before

56

@ once only. In case 5A the event ID of the αi in R is not equal to the associated event ID of αi in the reiterated state set of S; we have Γ(S)=∅.

In case 5B the event ID of the αi in R is equal to the associated event ID of αi in the reiterated state set of S. We have Γ(S)= Γ′′{S}, and the Γ′′

function is as follows:

 In addition to α0, α1, …, αn–1, if there is no new reiterated state in S, then we have Γ′′(S)=S.

 In addition to α0, α1, …, αn–1, if there is at least one new reiterated state in S, then Γ′′(S) performs the same transformation as for cases 1, 2, and 3.

• Case 6: Referring to Figure 19F, ∃ αi, 0≤i<n, αi appears before @ more than once; we have Γ(S)=∅.

• Case 7: If none of cases 1, 2, 3, 4, 5, and 6 holds, we have Γ(S)=S.

Theorem 6 indicates that the transformation of the Γ function can avoid boundless state reiteration and thereby achieve dynamic effective testing.

Theorem 6: Assume that a DFA F exists that represents the execution of a concurrent program P with input X. According to the framework in Figure 17, using the Γ function to perform SYN-sequence transformation before deriving race variants can achieve dynamic effective testing of P with input X, with the testing process eventually terminating.

Proof: We divide the proof of the theorem into three parts. In the first part of the proof we show that boundless state reiteration will not occur in the testing process.

Consider how the reiterated states are recorded. Assume that we can obtain a sequence of execution states from a SYN-sequence. Given a SYN-sequence S, we

first consider the situation that no state in the reiterated state set occurs in S. In cases 1 and 2, as shown in Figure 19A and B, the first-occurring reiterated state A will be stored in the reiterated state set of S1 and S2. However, there may be more reiterated states that occur after A, as shown in Figure 20A and B. We show one such state as state B. The race analyzer will derive race variants in all the execution states after @. We can then obtain race variants as shown in Figure 20C, D, and E.

The race variant in Figure 20C is obtained from the race analysis of states in the Pe of Figure 20A. The race variant in Figure 20D is obtained from the race analysis of states after the first state A of Figure 20A. The race variant in Figure 20E is obtained from the race analysis of states after the first state B of Figure 20B. We assume that the prefix-based replay of the three race variants reaches state B after

@ again as shown in Figure 20F, G and H, respectively. Without loss of generality we assume that state A occurred again. In case 4 of Γ, events after state A (which has been recorded as a reiterated state) are removed. In the case that state B reiterates after @ and is not removed as shown in Figure 20F, this will be recorded as a reiterated state in case 4 by Γ′. See Figure 20I. In case 5B of Γ we try to find the new reiterated state in addition to state A (which is recorded as a reiterated state).

Referring to Figure 20G and H, state B will be discovered and recorded as a reiterated state in case 5 by Γ′′. See Figure 20J and K. We have shown that state B will also be recorded in the reiterated state sets in these situations. Similarly, if there are also reiterated states after B that can be reiterated by the prefix-based replay, they will be recorded in the reiterated state set eventually.

As shown above, the found reiterated states will be recorded in the reiterated state

58

set of some SYN-sequences. The only exception is case 3 in Definition 6. However, since S is abandoned, reiterated state A will not cause boundless state reiteration.

The stored reiterated states are used to avoid boundless state reiteration, which corresponds to cases 4, 5A, and 6 in Definition 6. In case 4 we prohibit more state reiterations caused by αi by removing all the events after stored reiterated state αi. In cases 5A and 6, since the SYN-sequences are abandoned, reiterated state αi will not cause boundless state reiteration. Thus, boundless state reiteration will not occur in the testing if the SYN-sequence is transformed by Γ before it is used to

The stored reiterated states are used to avoid boundless state reiteration, which corresponds to cases 4, 5A, and 6 in Definition 6. In case 4 we prohibit more state reiterations caused by αi by removing all the events after stored reiterated state αi. In cases 5A and 6, since the SYN-sequences are abandoned, reiterated state αi will not cause boundless state reiteration. Thus, boundless state reiteration will not occur in the testing if the SYN-sequence is transformed by Γ before it is used to