Database Reference
In-Depth Information
Algorithm 2
Input:
A set T of concurrently executed transitions.
Output:
A partition of the transitions in T such that each partition class may lead to non-
confl uence.
(Note that once again our analysis is very conservative in the sense that theset N out-
putted by Algorithm 2 may not lead to non-confl uence. As in Algorithm 1, to conclude
that there is non-confl uence, we must carefully study the actual computations of the
transitions, which we do not perform here.)
1.
We fi rst create a graph G with each transition in T as a vertex in G. However, G has
no edge in this stage.
2.
If two distinct transitions t1 and t2 have a read-write racing problem or a write-
write racing problem, we add an edge to the two corresponding vertices in G.
We continue this step until no more edges can be added to G. Note that at most
n(n-1)/2 edges are added to G if n is the number of transitions in T.
3.
The transitions in each connected component of G with at least two transitions may
lead to non-confl uence.
Theorem 2.
Algorithm 2 correctly identifi es sets of transitions that potentially lead
to non-confl uence.
Proof:
Note that Algorithm 2 partitions the set T into disjoint subsets of T. Consider a
partition class C where C is a connected component in G. If C has at least two transitions,
then a transition in C has either a read-write racing problem or a write-write racing problem
with another transition in C. Switching the order of execution of these two transitions will
cause different fi nal states of the system.
We may repeat Algorithm 2 until the set T becomes empty. At that time, there are no
more transitions to be removed from T. Note that all the sets of transitions outputted by
Algorithm 2 that may potentially lead to non-confl uence have at least two transitions.
For any such set N and for any transition in N, there is another transition in N such that
they have either a read-write racing problem or a write-write racing problem. In this way,
Algorithm 2 points out the set of transitions that may potentially lead to non-confl uence to
the analyst and the analyst may consult with the client to devise a solution to the problem.
The next theorem is interesting in the sense that the statemate semantics of statecharts avoid
certain problems.
Theorem 3.
If a statechart S implements the statemate semantics, then read-write
racing problems will not cause non-confl uence.
Proof:
Since each transition is prioritized and calculations in one step are based on
the situation at the beginning of the step, and updates of data values only occur at the end
of a step, the data values read during the execution of a step are all produced in the previ-
ous step. Thus any data values produced during the execution of a step will not be read by
any transitions executed in the same step. Therefore, read-write racing problems will not
cause non-confl uence.
As an example, if the statechart in Figure 9 implements the statemate semantics, then
the calculation of the payment will be based on the old interest rate rather than on the new
