Partial Order Graph of SYN-sequence

For the purpose of verification, we may want to have a data structure that explicitly contains the inter-process dependencies or simply dependencies. At the same time, we want our data structure to maintain a minimal number of dependencies. This minimal set of dependencies can be determined by the Dependency Algorithm. This algorithm also gives a formal definition of our dependency relation.

Dependency Algorithm

4. Initialize the arrays head and tail to be null.

5. Figure out the three-dimensional arrays head and tail that stores the first and the last event, respectively, of each version number in each process. This is done by, for each event in each process , if event access variable of version and

c. if head[ ][ ][ ] is null or < head[ ][ ][ ], then modify head[ ][ ][ ] to store .

d. if tail[ ][ ][ ] is null or > tail[ ][ ][ ], then modify tail[ ][ ][ ] to store .

Note that the elements of both arrays may be null.

6. For each event head[ ][ ][ ], if it is not null and

a. if the operation is write, then add dependencies from the read events tail[ ][ ][ − 1] for all processes other than . If no such read

event and tail[ ][ ][ − 1] is also null, then add an dependency from the event tail[ ][ ][ 1] in which the operation is write.

b. if the operation is read, then add an dependency from the write event head[ ][ ][ ].

If any events in the dependency are null, then this dependency is ignored.

Figure 3.1. An example of partial order graph.

The path on the left simulates process 0, and the other one simulates process 1. The dashed line is the dependency additional to the SYN-sequence.

Figure 3.1 shows an example partial order graph of SYN-sequence. It is obvious that before w( ,1) of process 0 being executed, all access to variable with version 0 must be finished. Thus we have a dependency from r( ,0) of process 1 to w( ,1) of process 0. This illustrates step 6a in the algorithm.

Now all access to variable with version 1 can proceed in process 0. After that, process 0 must wait before executing w( ,3) until all access to variable of versions less than 2 is completed. In this case, we add a dependency from r( ,2) of process 1 to w( ,3). This also followed the step 6a. Similarly, we have a dependency from r( ,1) of process 0 to w( ,2) of process 1. Before executing r( ,3) of process 1, we must make sure that w( ,3) was ever executed and thus add the necessary

0

dependency. This illustrates step 6b in the algorithm. Note that each write to a variable of a specific version will appear in the SYN-sequence exactly once.

What if we have other processes that are not shown and all access to variable of version 2 in process 1 becomes r( ,1) as in Figure 3.2? One may thought that we have to add a dependency from the latest r( ,1) in process 1 to w( ,3) of process 0.

Addition of this dependency is, however, redundant since we are confident by our algorithm that we do have a dependency from r( ,1) of process 1 to w( ,2) in certain process, and some dependency may exist till we have one or more dependency to w( ,3).

Figure 3.2. Event w( ,2) occurs in some process other than processes 0 and 1.

Note that all events within the same process must be executed in strict order according to their event identifiers. This is why we restrict the term “dependency”

between only events of different processes.

0

1

0

1 w( ,1)

r( ,1)

2 2

r( ,1)

3 3

w( ,3)

r( ,0)

r( ,1)

r( ,1)

r( ,3)

w( ,2)

Figure 3.3. The partial order graph of SYN-sequence.

We assume the values of are 4, 7, 11 respectively when the versions are 0, 1, 2. The value of is constantly 3.

Now let’s see one more example to gain insight into the behavior of the SYN-sequences. Figure 3.3 shows a SYN-sequence in the form of partial order graph.

Initially, the first event of process 0 or process 1 may be executed. However, the execution of event 0 in process 1 must be postponed after the execution of event 1 of process 0. Hence the first executed event is event 0 of process 0. After that only the event 1 of process 0 could be executed. Now it’s time for event 0 of process 1 to be executed.

The three events are executed in a fixed sequential order, and then one of event 2 in process 0 and event 1 in process 1 can be nondeterministically chosen for executing.

Some properties exist in SYN-sequence. The first one is happened before relation. If two events must be executed in the fixed sequential order, we say that the prior one must

happen before the posterior one. The edges on the partial order graph of SYN-sequence

present the happened before relation. Event happens before event iff there exists a path from to on the partial order graph. The second property is parallel relation. If two events can be nondeterministically chosen for executing, we say these events are

parallel. Events and are parallel iff there exists no path between to on the partial

order graph. This is obvious by definition, since no paths existing between these two events implies no strict execution order for these events. The third property is transition

0

relation. This property is, however, not explicitly presented in the partial order graph at all. Even there exists a path between two events, one of these events may not happen

directly after the other. This is illustrated by events 1 and 2 of process 0 in Figure 3.3,

since event 2 can be executed only if both event 1 of process 0 and event 0 of process 1 were executed, while event 1 of process 0 always happens before event0 of process 1.

On the other hand, if there is no path between two events, one of the events may be executed right after the execution of the other. In Figure 3.3, e.g., once event 2 in process 0 or event 1 in process 1 was executed, the other one can be immediately chosen for executing.