Think Stitch


Dynamic Creation of Processes 2

This is the second article for the Dynamic Creation of Processes in SyncStitch and CSP.

Continuation of the Parent Process

When child processes are created by the parallel composition, the parent process gets into the wait state for the child processes, and terminates after the terminations of all child processes. However, it is often the case that we want the parent process to continue after the terminations of the child processes in order to do another jobs. We can achieve this using the parallel compositions and the sequential compositions.

The process P described below creates two child processes when it receives an event c. At the same time, P specifies the continuation process after the terminations of the child processes with the sequential composition seq. When all of the child processes terminate, the seq shifts to the continuation process.

(define-process P
  (! c
     (seq
       (par '()
         (! a1 SKIP)
         (! a2 SKIP))
       (! b SKIP))))

The computation tree of P is as follows. The state labelled with A is the state in which two child processes have terminated. From the state A, the par terminates, the process tree is folded, and the seq shifts to the continuation (! b SKIP), which is the state labelled with B.

In the case that you want to pass data from the state A to the state B, you can do it with a memo process.

Parent-Child Processes Revisited

Consider the process which creates a child process Q and waits for the termination like a shell in UNIX-like operating systems again. This time we executes the process Q twice.

(define-process P
  (! c
     (par (list b)
       Q                         ; the first instance
       (! b                      ; waits for the termination
          (! c
             (par (list b)
               Q                 ; the second instance
               (! b SKIP)))))))  ; waits for the termination and terminates.

(define-process Q
  (! a (! b SKIP)))

This process has a deadlock! Could you tell why it deadlocks?

The computation tree is as follows:

In the selected state, the second instance of the process Q is about to generate an event b, the termination notification. However it cannot occur. You can see this in that the state is colored with green, which means there is no transition from the state, even though the parent process is ready to accept the event b. Can you spot the problem?

Since the both two par nodes on the process tree have the event b in the synchronization lists, the occurrence of the event b needs participation of the first instance of the process Q which had already terminated. In other words, the occurrence of the event b is the simultaneous synchronization of three processes. In general, more than two processes can synchronize on an event in CSP. Unfortunately, this characteristics of CSP caused the problem.

Solution 1

One of the solutions to this problem is to use different events for different instances of the process Q. Suppose, for example, we have events b1 and b2. We also need to divide the definitions of the instances of the process Q since the notification events differ.

(define-process P
  (! c
     (par (list b1)
       Q1
       (! b1
          (! c
             (par (list b2)
               Q2
               (! b2 SKIP)))))))

(define-process Q1
  (! a (! b1 SKIP)))

(define-process Q2
  (! a (! b2 SKIP)))

No deadlock is found this time.

The second instance of the process Q can successfully terminate.

Solution 2

If two child processes run concurrently, it is necessary to use different event for each child process to distinguish which child is terminated. However, if child processes are executed sequentially, it seems to be a waste to use two events. Since the processes are executed sequentially, the problem is solved using the sequential compositions.

We can combine the execution of the two instances of the process Q by seq. By doing this, we can share a event b in the two executions.

(define-process P
  (seq
    (! c
       (par (list b)
         Q
         (! b SKIP)))
    (! c
       (par (list b)
         Q
         (! b SKIP)))))

(define-process Q
  (! a (! b SKIP)))
3 August, 2013