Pre-Condition: DB4op has been calculated by Algorithm 11 Set of Operation Sets CDBOPS {
01: DB4OPSop = Ø;
02: duplicate DB4op to BaseSet;
03: while( BaseSet ≠ Ø) { 04: CurrentOPS = Ø;
05: choose and remove arbitrary operation op’ from BaseSet;
06: duplicate DB4op \{op’} to CountSet;
First, the algorithm duplicates DB4op to BaseSet at line 2. The codes from line 3 to 16 form a loop. In the loop, an operation op’ is arbitrarily chosen from BaseSet, and all the operations
concurrent to op’ and each other are gathered and put into CurrentOPS. CurrentOPS is added to the result set as one of the operation sets found by the algorithm at the end of the loop. The operations in CurrentOPS are removed from BaseSet, and the next loop starts if there is still operation remaining in BaseSet. Because any operations in DB4op are mutually concurrent or exclusive, the operation chosen in the next loop is exclusive to at least one of the operations gathered in this loop. Besides, the algorithm starts collecting an operation sets from different operations every loop, and thus none of the operation sets collected in Algorithm 12 are identical. After each operation in BaseSet is distributed into some operation set, the algorithm returns the calculated DB4OPSop at line 17.
To depict the correctness and the effectiveness of Algorithm 12, we show that the following lemmas hold.
Lemma 9
The result set returned by Algorithm 12 follows Definition 28.
Proof:
Let OPS be one of the operation set collected in CDBOPS(op). According to the pre-condition of Algorithm 12, DB4op has been calculated by Algorithm 11, and according to Lemma 1, Definition 10, and Definition 26, the operations in DB4op are either mutually concurrent or exclusive. From line 7 and line 11 of Algorithm 12, we know that all the operations collected in OPS are mutually concurrent. The operations gathered in OPS are removed from BaseSet at line 12. Therefore, for any operation remaining in BaseSet, there exists at least one operation exclusive to it in OPS. Because BaseSet is duplicated from DB4 at line 2, OPS follows Definition 28, and Lemma 9 is thus shown correct. □
Before Algorithm 12 is introduced, four possible cases of the set of operation sets derived from DB4op are described, and we claim the capability of Algorithm 12 based on the cases.
Here, we show the claim holds with the following lemma.
Lemma 10
Algorithm 12 is able to find the operation sets for case (1), (2), and (3) completely, and for case (4) partially.
Proof:
The cases are separately discussed as following:
(1) All the operations in DB4op are concurrent to each other.
In this case, the algorithm collects all the operations in the first loop of the algorithm. Only one operation set is included in the result set of Algorithm 12.
(2) All the operations in DB4op are exclusive to each other.
In this case, an operation is collected in an individual operation set in each loop. Let the size of DB4op be N. As the result, N particular operation sets are collected in DB4OPSop, and the union of the sets is identical to DB4op.
(3) The operations in DB4op can be divided into several distinct groups where the operations in the same group are concurrent to each other, and the operations belonging to different groups are all mutually exclusive.
In this case, DB4op can be divided into several distinct operation sets following Definition 28. However, the operations included in different sets are all mutually exclusive. According to Lemma 9, the operation sets collected by Algorithm 12 follow Definition 28. On the basis of the algorithm, each operation in DB4op is collected into some operation set in DB4OPSop. Therefore, all the operation sets in this case can be found by Algorithm 12.
(4) The operations in DB4op can be organized into several varied groups where the operations in the same group are concurrent to each other, and the operations belonging to different groups are either identical or mutually exclusive.
In Algorithm 12, at least one operation is removed from BaseSet in the loop starting from line 3, and therefore the algorithm derives at most N operation sets from DB4op. For case (4), the number of operation sets identified by Algorithm 12 is less than N, but the number of operation sets in this case might exceed N. The decision structure where no process residing in the branch has operations effective on the same artifact, is still ignored. Figure 15 illustrates parts of an LRTS workflow that the definitions made by v1 and v2 are directly before the usage made by v4. The definitions should be considered separately during analysis because they are exclusively executed during run-time.
However, if the third branch is taken during execution, the usage made by v4 is undefined because the definition of a is killed by v0, and no further definition is made by activity processes on the third branch. The third branch is a blank branch which generates a blind spot in our methodology.
Figure 15 An Example of a Blank Branch
For any operation op, to eliminate the effect brought by blank branches when calculating its input states, all the operations reside in the decision structure with blank branches should be removed from OPLop, and DB4op can then be recalculated for analysis. Algorithm 13 detects blank branches from the directly before operations of the input operation.
Algorithm 13 Detecting Blank Branch - DBB