The information required about synchronization events for

A scheme for replaying sequence of read and write operations of shared-memory concurrent programs has been presented elsewhere [38]. It is referred to as “instant replay”, in which only the version number of the accessed variables should be recorded.

For race analysis in reachability testing, the name and version number of the accessed shared variable must be recorded [30,31,32]. As mentioned in Chapter 3, read and write events are denoted R(U,V) and W(U,V), respectively, where U and V are the name and version number of the variable. In general, the variable name and version number in a synchronization event are sufficient to generate race variants for exploring feasible interleavings, since the variable name can recognize if two events could race and we can rearrange their order by changing the version numbers to produce race variants.

66

However, to avoid boundless state reiteration, the Γ function must examine the execution states. According to Definition 4, the execution location of the read or write operation in the program context and the value of the accessed shared variable must be recorded in the synchronization event to derive the execution states. An intuitive approach would be to only record the read and write operations of shared variables in the SYN-sequence, since the nondeterminism of the concurrent program only depends on the interleaving of operations to shared variables. However, it is not sufficient if we want to identify the reiterated states. Consider the concurrent program in Figure 23. Note that statement “^write(a,1)” involves writing the value “1” to variable a, and statement

“^T1=read(a)” reads the value of variable a and assigns it to variable T1. Consider the following two execution sequences of statements of this program: ES1= {S1,0, S0,0, S0,1, S1,1} and ES2={S1,0, S1,1, S0,0, S0,1}; note that a is the only shared variable. If we do not consider local variables T1 and T2, the execution states after ES1 and ES2 are the same;

that is, {(S0,1, S1,1),(a=1)}. However, if we consider the local variables, the execution states after ES1 and ES2 are {(S0,1, S1,1), (a=1, T1=1, T2=1)} and {(S0,1, S1,1), (a=1, T1=1, T2=0)}, respectively. In the former case, T2 equals 1, and process P1 exits the

while loop. However, in the latter case, where T2=0, process P1 will iterate one or more times. To avoid this problem, we may consider recording all the read and write operations of local and shared variables in the SYN-sequence. However, the presence of too many events in the SYN-sequence increases the analysis time of the Γ function.

Below we discuss how to record essential information about synchronization events to support the operation of the Γ function.

a is a shared variable whose initial value is 0.

Figure 23. The transformed concurrent program of Figure 1B

In a high-level programming language, a single statement can contain multiple events.

For example, if SV1, SV2, and SV3 are shared variables, then the statement “SV1=SV2+SV3” will issue three synchronization events: two read operations of SV2 and SV3, and one write operation to SV1. We have to perform a simple transformation of the target program to ensure that each statement contains at most one synchronization event for the following reasons. First, the existing algorithms for race variant generation assume that a statement contains only a single synchronization event [30,32,34]. Second, a single operation can deterministically make an execution state transition. According to the Γ function, we transform the target program according to the following atomic-synchronization-event-transformation (ASET) rules:

• Rule 1: We have to record all the write operations to local and shared variables, since a write operation to either a local variable or a shared variable always causes a transition of the execution state.

• Rule 2: Only read operations of the shared variables need to be stored in the SYN-sequence. Although the read operation of a shared variable does not change the value of any variable, we need it to store in the SYN-sequence in order to explore interleavings.

• Rule 3: A statement that contains multiple operations that should be recorded is decomposed into several statements, each of which contains a single operation. Note that we may need to use some temporary variables to perform the statement decomposition. Data movements between temporary variables do not need to be recorded in the SYN-sequence.

68

• Rule 4: Write operations to variables take the form

“write(V,LV_or_Constant)”, where V is the name of a variable and LV_or_Constant is the name of a local variable or a constant whose value is written to V. Read operations of shared variables take the form

“LV=read(SV)”, where SV is the name of a shared variable and LV is the name of a local variable to which the read value of SV is written. For example, statements such as {SV1=SV2+SV3;} can be transformed into {T1=read(SV2); T2=read(SV3); T3=T1+T2; write(SV1,T3);}, where T1, T2, and T3 are temporary variables. The “write(V,LV_or_Constant)” and

“LV=read(SV)” operations execute the entry and exit protocols for the prefix-based replay. In the monitor phase, the protocols will store a synchronization event in the SYN-sequence. According to this rule, a write operation to a shared variable must be from a local variable.

• Rule 5: The read and write events stored in the SYN-sequence are denoted R(U,V,L,C,T) and W(U,V,L,C), respectively, where L is the execution location of the read or write operation in the program context (there can be distinct labels for each read and write operation), C is the value of the accessed variable (i.e., the value read or written in a read or write operation, respectively), and T is a local variable to which the value read is assigned. The

“write(V,LV_or_Constant)” and “LV=read(SV)” operations will store a write event W(U,V,L,C) and read event R(U,V,L,C,T) in the SYN-sequence, respectively.

• Rule 6: The Boolean predicates in the loop or conditional branch construct should not contain read operations of shared variables or write operations to any variable. As a result, the Boolean predicate in the transformed program is a function that only reads some local variables.

According to the ASET rules, the concurrent program shown in Figure 1B is transformed into the program shown in Figure 23. Note that the original Boolean predicate is “^a==0”, which contains a read operation of shared variable a. In the

transformation, we insert a statement “^T1=read(a)” before the Boolean predicate, and then new Boolean predicate “^T1==0” performs the equivalent operation. It is obvious that not all the execution locations of processes are revealed in the SYN-sequences. The read operations of local variables are not included in the SYN-sequence. For example, the evaluation of the Boolean predicate is not recorded in the SYN-sequence, which means that we cannot obtain all the possible execution states of the target concurrent program.

In fact, the recorded SYN-sequences can only allow us to derive the execution state after each recorded event. However, the transformation performed according to ASET rules does not result in dynamic effective testing being unable to achieve the goal of state-cover testing. Section 5.6 provides further discussion and proof.

5.4.2. Deriving a unique totally ordered sequence of execution states from a