The correctness of the proposed scheme

In [32], Hwang et al. employs the maximum common feasible prefix (MCFP)²⁴ to prove that reachability testing will derive all of the feasible SYN-sequences.

Consider two SYN-sequences T1 and T2. TMCFP is the MCFP of T1 and T2 if TMCFP is a feasible prefix of both T1 and T2, and has the maximum number of synchronization events. The MCFP defined in [32] is based on a T-sequence that contains events of an SQL transaction. We need another algorithm to derive the MCFP based on sending and receiving events; this algorithm is listed as Algorithm 12. Figure 35 offers some examples to demonstrate the MCFP.

Consider two feasible SYN-sequences S1 and S2 of a concurrent program P with input X. S2 can be derived from S1 using the following steps. The race analysis of S1 can yield at least one race variant R1, which is a feasible prefix of S2, where |R1|²⁵>|MCFP of S1 and S2|. The prefix-based replay of R1 produces SYN-sequence SR1, and we have |MCFP of SR1 and S2|≥|R1|. The race analysis of SR1 will yield at least one race variant R2 that is a feasible prefix of S2, where |R2|>|MCFP of SR1 and S2|. This process is repeated, which yields |MCFP of SR(i+1) and S2|≥|R(i+1)| and |R(i+1)|>|Ri|, i≥1. We will continue this process to obtain longer feasible prefixes of S2 and eventually obtain S2 itself.

24 See Definition 5 in [32].

25 |R| means the number of synchronization events in R.

94

Figure 35. (A) Another example SYN-sequence that contains multiple receivers. (B) The partial order graph of Figure 30. (C) The partial order graph of Figure 35A. (D) The

MCFP of the SYN-sequences in Figure 30 and Figure 35A.

Algorithm 12: Generate the MCFP of two SYN-sequences S1 and S2

Input: SYN-sequences S1 and S2 containing two types of synchronization events:

sending and receiving.

Output: The maximum common feasible prefix of S1 and S2.

(1) Invoke Algorithm 11 to generate the partial order graphs of S1 and S2, which are designated PG1 and PG2, respectively.

(2) Let SMCFP be a SYN-sequence with no event.

Definition 9: Let PG be a partial order graph derived from a SYN-sequence. Event e is a not-happened-before event if no event happened before e in PG.

Before we present the formal proof of the correctness of Algorithm 10, we need several lemmas that demonstrate some properties about the MCFP of two SYN-sequences. In Lemma 1, we see that the two sets of not-happened-before events after the MCFP of two SYN-sequences must be identical receiving events.

Lemma 1: Assume that there are two SYN-sequences Sx and Sy. Let SMCFP be the maximum common feasible prefix of Sx and Sy. (Sx-SMCFP) and (Sy-SMCFP) are the event sequences of Sx and Sy obtained by removing the events in SMCFP, respectively.

Then,

(1) All not-happened-before events in (Sx-SMCFP) and (Sy-SMCFP) are receiving events.

(2) The set of not-happened-before events in (Sx-SMCFP) is equal to the set of not-happened-before events in (Sy-SMCFP).

Proof: We first assume that there exists a sending event s that is a not-happened-before event in (Sx-SMCFP) and (Sy-SMCFP). Below we show that it is impossible for s to be a sending event. Let s be an event executed by process Pi. We use s.ts[i] to denote the i-th element in the vector timestamp of event s. Let e be the previous event of s;

that is, process Pi executes s after e. Since s is a not-happened-before event in (Sx-SMCFP) and (Sy-SMCFP), e is located in SMCFP and has the same vector timestamp in Sx and Sy. Note that we assume that s is a sending event. Thus, according to the

96

timestamp assignment rule [36], the vector timestamps of s in (Sx-SMCFP) and (Sy-SMCFP) should be derived as follows: s.ts[k] = e.ts[k] where k ≠ i, and s.ts[i] = e.ts[i]+1. If the vector timestamp of s is the same in (Sx-SMCFP) and (Sy-SMCFP), then s should be in SMCFP. This contradicts our earlier assumption. Therefore, if s is a not-happened-before event in (Sx-SMCFP) and (Sy-SMCFP), it must be a receiving event.

Second, since SMCFP is a common feasible prefix of Sx and Sy, we must reach the same execution state after the execution of SMCFP in Sx and Sy. Then, all of the events that can be executed without waiting for other events in (Sx-SMCFP) and (Sy-SMCFP) must be identical. Therefore, the set of not-happened-before events in (Sx-SMCFP) is equal to the set of not-happened-before events in (Sy-SMCFP). QED

In [36], Lei and Carver defined the port used in the FIFO message ordering scheme, which guarantees that the messages are received in the order that they are sent. Assume that si and sj are sending events and rp and rq are receiving events of the same port. If si

has happened-before sj and rp has happened-before rq, then it is impossible that rq

received the message from si or that rp received the message from sj. Based on the FIFO message ordering scheme of the port, we show another property in Lemma 2—that there must be a race between the events, which are the not-happened-before events after the MCFP of two SYN-sequences. Figure 36 is used to illustrate Lemma 2.

The sending partner of rα in Sx is identical to the sending partner of rβ in Sy.

s_p

rα rβ

Sy

Sx

SMCFP

∆

S_x-S_MCFP S_y-S_MCFP

s_p

rα rβ

The transmission of a message

Figure 36. An example is with two SYN-sequences Sx and Sy. There must be two receiving events, which are not-happened-before events (∆), racing for the same

message from the sending event in SMCFP.

Lemma 2: Assume that there are two feasible SYN-sequences Sx and Sy of a concurrent program with the same input. Let SMCFP be the MCFP of Sx and Sy. (Sx-SMCFP) and (Sy-SMCFP) are the event sequences of Sx and Sy after removing the events in SMCFP, respectively. According to Lemma 1, let the set of not-happened-before events in (Sx-SMCFP) and (Sy-SMCFP) be ∆. rα is a receiving event in ∆, and it received the message from sp in Sx. Assume that the port complies with the FIFO message ordering scheme. There must be a receiving event rβ in ∆ where the sending partner of rβ in Sy is sp.

Proof: We first prove that rβ must be in Sy. Assume that rβ is not in Sy. Then, there is no receiving event that races against rα in Sy. Since rα is a not-happened-before event in ∆, rα must be the only receiving event of sp after the execution of SMCFP. Thus, rα must receive the message from sp. Let rα is performed by process Pi and e be the event executed by Pi that just happened-before rα. Referring to the timestamp assignment scheme, the vector timestamp of rα is computed from the vector timestamps of e and its sending partner. Thus, the vector timestamp of rα in Sx is identical to the vector timestamp of rα in Sy, and rα must be located in SMCFP. It is

98

a contradiction that rα is not in SMCFP; that is, there must be a receiving event rβ

that is racing rα to receive a message from the same port in Sy.

Second, we prove that rβ must be located in ∆. We assume that rβ is not located in

∆ and that rβ received the message from sp. There are two cases for the location of rβ: (1) rβ is located in SMCFP and (2) rβ has happened-after rα. In the first case, according to SMCFP being the common feasible prefix of Sx and Sy, rβ must receive the message from sp in Sx. This is a contradiction to the hypothesis that rα received the message from sp in Sx. In the second case, there are two feasible SYN-sequences Sx and Sy' (see Figure 37). The message from sp is the first out message after the execution of SMCFP based on the nature of the FIFO message ordering scheme. That is, the execution of rβ must not receive the message from sp

since rβ has happened-after rα. This contradicts the hypothesis that rβ received the message from sp in Sy'. Thus, we can conclude that for any two SYN-sequences Sx

and Sy there must be a receiving event rβ in ∆, and that the sending partner of rα in Sx is identical to the sending partner of rβ in Sy. QED

s_p

r_α

r_β Sy' Sx

S_MCFP

S_y'-S_MCFP

∆ s_p

r_α

Figure 37. An example is with contradiction in SYN-sequence Sy'. According to the nature of the FIFO message ordering scheme, the receiving event rβ must not receive the

message from sp since rβ has happened-after rα.

Based on Lemma 2, we can have Lemma 3, and then we can present Figure 38

illustrates this lemma.

Lemma 3: Based on Figure 38, assume that the identical sending partner of rα and rβ

is s_p. If sending event s_k happened-before s_p and both sent a message to the same port, then the receiving partner of sk must be in the MCFP of Sx and Sy.

Proof: Referring to Figure 38, since sk has happened-before sp and both sent a message to the same port, the receiving partner of sk (i.e. r) must have happened-before rα

based on the nature of the FIFO message ordering scheme. That is, it is impossible for r to be a not-happened-before event in (Sx-SMCFP) or (Sy-SMCFP).

Thus, the receiving partner of sk is in the MCFP of Sx and Sy. QED

sp

rα r

β

S_y S_x

SMCFP

∆

S_x-S_MCFP S_y-S_MCFP

sp

r_α r_β

s_k r

s_k r

Figure 38. For a sending event sp, if (1) the message from sp is raced by the events in ∆ and (2) a sending event sk sent message to the same port as sp and happened-before sp,

then the message from sk would be received by the event in SMCFP.

Theorem 8: Assume that the number of feasible SYN-sequences of a message-passing program P with input X is finite and that every execution of P with input X terminates.

The reachability testing of P with input X can enumerate all of the feasible SYN-sequences of P with input X if we apply Algorithm 10 to derive race variants.

100

Proof: Assume that we have a SYN-sequence S of P with input X. Since every execution of P with input X terminates, the number of events in S must be a positive integer, which we denote as |S|. Assume that S' is another feasible SYN-sequence of P with input X. Below we prove that we will eventually conduct a test on S' if we apply Algorithm 10 to derive race variants.

Let SMCFP be the MCFP of S and S', and |SMCFP| = m, where m is a positive integer.

It is trivial that m ≤ |S| and m ≤ |S'|. Without loss of generality, if m > 0 then there must be a synchronization pair <si,ri> in S, where ri is a receiving event in the set of not-happened-before events in (S-SMCFP). According to Lemma 2, there must be a receiving event rj in ∆ of (Sy-SMCFP) where the sending partner of rj is si. Note that ri and rj receive messages from the same port.

When we apply Algorithm 10 to derive race variants from S, all possible happened-before relations would be derived in step (2) because we apply a topological sort to derive all valid total orders of the receiving events of the same port. There must exist a total order in which rj has happened-before ri. Below we show that rj must be in the race set of ri. According to Algorithm 10, we employ the rules in [36] (i.e. φ1–φ4) to generate the race set of ri. Since si, ri and rj access the same port and si is in SMCFP, si conforms to rules φ1 and φ2. Rule φ3 also conforms because the generated total order rj has happened-before ri. For rule φ4, all of the receiving partners of the sending events that happened-before si are in SMCFP and happened-before rj based on Lemma 3. Then, rj is in the race set of ri. Thus, we show that the derived race variants include a feasible prefix (SMCFP+rj) of S'.

The reachability testing will conduct a prefix-based replay of (SMCFP+rj). Assume that this produces a SYN-sequence S1. It is trivial that (SMCFP+rj) is a feasible prefix of S1 and S'. Let SMCFP+1 be the MCFP of S1 and S'. It is obvious that

|SMCFP+1| ≥ |SMCFP|+1 = m+1. Again, applying Algorithm 10 to S1 will derive a race variant of size |SMCFP+1|+1. Repeating the above process will eventually produce a SYN-sequence that is equal to S' in the prefix-based replay. QED

102