Think Stitch


Alphabetized Parallel Compositions

In this article, I will explain alphabetized parallel composition operator apar and its quantifier version xapar, which are supported in SyncStitch version 1.1.0.

In the SyncStitch Users Guide, the alphabet of a process is explained to be a set of all events used in a model. It is represented as the symbol Σ. Actually there are two styles to see what an alphabet is. One is what is explained in the Users Guide, on which the alphabet means the set of all events used in a model. Another is a style which is explained in the Hoare's book Communicating Sequential Processes, on which each process has its own alphabet. On the latter style (the Hoare's style), the alphabet of a process P is represented as α(P). ('α' is a greek letter alpha. It might be a little hard to see in some browsers.)

There are some differences in the CSP theory depending on which style is used in the theory. When you read a CSP book, I advise you to check which style is adopted in the book.

The parallel compositions described by the operator par are called interface parallel compositions in contrast to the alphabetized parallel compositions. The difference is how to specify the events on which the combined processes synchronize.

In the case of the interface parallel, the events to be synchronized are specified as a sync-list. On the other hand, in the case of alphabetized parallel, a series of sets of events are specified corresponding to a series of processes to be combined. In other words, a set of events is specified for each process which uses the events in the set.

In the CSP theory, the alphabetized parallel is represented as follows:

P and Q are processes to be combined. A is a set of events to be used by P and B is by Q. In SyncStitich, it is described as follows:

(apar A P B Q)

I will explain what process this expression means from here.

Alphabets of Processes

When you define a process by process expressions, the set of events the processes use is inherently determined. For exmaple, concider the following process:

(define-process P
  (alt (! a STOP) (! b (! c STOP))))

This process has the ability (possibility) to generate the events a, b, and c. It can be said in Hoare's style that the "alphabet" of the process is α (P) = {a, b, c}. In the alphabetized form apar, we specifiy the alphabet apart from the inherent "alphabet".

When the alphabet A is specfied in a apar form, the corresponding process P can generate only the events in A. Even if the process P has the ability to generate an event out of the alphabet A, it is inhibited.

When we call the inherent "alphabet" determined from the process expressions X, the actual events the process can generate in the apar form is equal to the intersection of X and A, which is designated with the orange-colored area in the following figure. The events in the outside area of X (A ∖ X) cannot be generated since the process has no ability to do it. The events in the outside area of A (X ∖ A) are inhibited.

This is the basics of the alphabetized parallel compositions.

The Distinction between Synchronous and Asynchronous Communications

Firstly, I will explain the case where there are two processes.

(apar A P B Q)

In general, the relation between A and B are as follows:

On the events in the intersection of A and B, the process P and Q must synchronize. In other words, the events in the area can occur if and only if the both processes can generate them. On the other hand, the events in A ∖ B or B ∖ A can occur whenever the process P or Q can generate them respectively. This is the rule of the alphabetized parallel compositions. Roughly speaking the following formula holds:

(apar A P B Q) = (par (A ∩ B) P Q)

Let's see an exmaple:

(define-process P0
  (apar
    (list a b)
    (alt (! a SKIP) (! b SKIP) (! b1 SKIP))
    (list a c)
    (alt (! a SKIP) (! c SKIP) (! c1 SKIP))))

The first process of the apar form can generate only events a and b. In order to see the apar's ability to prevent events out of the alphabet from happening, the event b1 is specified in the process expression. The second process also defined like the first one. The event a is common in both alphabets and therefore it must be synchronized. The computation tree of the process is as follows:

 
 
 

You can see that the event a is certainly synchronized, and b and c occur independently.

The rule for the terminations of the apar form is the same as the par form.

In the case of combining more than three processes in parallel

Alphabetized parallel would merely be a syntax-sugar if it could be described using interface parallel. Actually, this is not because alphabetized parallel can restrict occurrence of events. Apart from that, alphabetized parallel itself is useful because each process can concentrate on specifiying its own alphabet, especially in cases where more than two processes are present. On the other hand, in the case of interface parallel, we had to consider the order in which the processes were combined.

You can specify more than two processes in apar forms. The general form of the apar operator is defined as follows:

(apar A1 P1 A2 P2 A3 P3 ...)

As you see, you specify any number of pairs of an alphabet and a process alternately.

The synchronization rules are as follows:

Let's see the case where three processes are present:

(apar A P B Q C R)

Let A, B, and C be alphabets. The relations among them are as follows:

Let's see a specific example.

(define-process P1
  (apar
    (list a ab ca abc)
    (alt (! a SKIP) (! a1 SKIP)
         (! ab SKIP) (! ca SKIP) (! abc SKIP))
    (list b bc ab abc)
    (alt (! b SKIP) (! b1 SKIP)
         (! bc SKIP) (! ab SKIP) (! abc SKIP))
    (list c ca bc abc)
    (alt (! c SKIP) (! c1 SKIP)
         (! ca SKIP) (! bc SKIP) (! abc SKIP)) ))

The computation tree of the process is as follow. You can zoom it by clicking.

The quantifier version of the alphabetized parallel composition operator xapar

The operator xapar is a quantifier version of apar. You can combine variable number of processes with alphabets by using it. The syntax of xapar is defined as follows:

(xapar var range A P)

The parameters var is a dummy variable. The parameter range is an expression evaluating to the range of the variable var. The process expressin P and the alphabet A can generally contain the variable var.

2013/12/23