3. SYN-sequences
3.3 Reachability Graph
We define a trace as a feasible totally-ordered execution sequence of events in the SYN-sequence, as well as an initial state that represent a system status before any event being executed and the states that keep track of the system status after the completion of each event. The recorded system status may be the values of all share variables, program counters of all processes, and the properties about executed events… etc. What to be kept in a state is on demand. If all information kept in a state is equal to that in another state, we say these states are equivalent. The term feasible indicate that the trace must follow all rules on the SYN-sequence, e.g. the dependency relation and the sequential property in each process. We can represent the trace as a path, where a node represents a state and an edge represents an event. Due to the nondeterministic behavior of concurrent programs, it is possible to figure out more than one trace in a SYN-sequence.
A reachability graph of a SYN-sequence is a representation of the transition system , , , where is the set of all states in all traces of that SYN-sequence, is the set of all initial states, i.e. the states before the execution of any event, is the set of transitions between two states, and is a function that labels each transition with an
event. The reachability graph of a given SYN-sequence comprises all traces from that SYN-sequence, while the events are labeled on edges whereas the identical paths are merged into a single one. Two paths in the reachability graph of a SYN-sequence are
identical if all states in both paths are equivalent and the sequence of events labeled on
both paths is identical. Each path in a reachability graph must be a trace of that SYN-sequence as well. For any state in the reachability graph of SYN-sequence, a
trace to is a path from any initial state to .
There are two models of reachability graphs according to the records kept in each state. A stateless model involves only the program counter expansion while a general or
stateful one involves variable value expansion as well. The program counter expansion
is the procedure that enumerates all possible traces from a SYN-sequence. Hence we can transform the partial order graph into reachability graph by program counter expansion.
Figure 3.4. The reachability graph of SYN-sequence as in Figure 3.3.
The numbers in each node are the values of variables and (in the upper line) and program counters of each process.
To carry out the variable value expansion, we need maintain the values of all variables. The properties about all variables are stateful properties. In practice, states in a stateless model keep track of only stateless properties, i.e. information about an event.
Let’s see the difference between stateful and stateless properties. As mentioned, each event may be associated with an operation type, an accessed share variable, a version number, a program counter… etc. Such data are stateless properties. When an event is
0,0 0,1 1,0 0,2 0,3
0,2 0,3
0,2 0,3
1,1 1,1
1,2 1,2
1,3 1,2
1,1
executed, the values of all variable are nondeterministic. For instance, see Figure 3.4.
When event 1 of process 1 is reading variable , the value of variable may be 7 or 11, depending on which state the system is in. In this thesis, the stateful properties kept in stateful model includes version numbers and values of all variables in each state; the stateless properties kept in both stateful and stateless model includes event counters, i.e.
identifiers of lastly executed events, and program counters of all processes.1
Theorem 1 For any states and in the reachability graph of SYN-sequence, if
both traces to and are comprised of the same set of events, regardless of the execution order, then and must be equivalent.Proof: If any two traces are comprised of the same events in the same execution order,
then these two traces are identical by definition. Otherwise, since both traces, say and , to and are comprised of the same events, the maximal event identifier of each process and the maximal version number of each variable in both paths must be the same as well. Since the event with maximum identifier must be executed lastly among those in the same processes, the event counters of all processes kept in and must be identical. Furthermore, the event with maximum version must be executed lastly among those on the same variable , the value of is identical in andThis theorem provides a scheme to identify each state other than using all information kept in that state; i.e. we can identify each state by using the set of events executed thus far. In other words, if the traces to states and comprise the same
1 The identifier of lastly executed process is also kept in each state of our implementation of SYN-verifier so that the operation, identifier, version number and value of shared variable lastly accessed are available in each state. This will be discussed in Chapter 1. Even so, we assume the properties of the lastly executed process are absent in the theoretical discuss in this chapter.
events, and are said to be identical. In reachability graphs, identical states are merged into one single state.
Theorem 2 For any state in the reachability graph of SYN-sequence, it is possible that
there exist more than one trace to this state. In such case, these traces are comprised of the same events while the execution orders are different.Theorem 2 are informally proved since we have an instance shown in Figure 3.4 We can easily see the lattice property, which is the natural consequence of theorems discussed thus far, in all reachability graphs.
Theorem 3 All traces of a SYN-sequence terminate in an identical state.
Proof: Since all events in a SYN-sequence must be executed, no matter what execution
order the events are in, all traces arrive at an identical state after the execution of all events in a SYN-sequence.The reachability graph of the example SYN-sequence shown in 3.1 is shown in Figure 3.4 based on the previous theoretical discussion.